From 4323e7d09fe2a3492587846194f7b9fb724ce789 Mon Sep 17 00:00:00 2001
From: Michael Sippel <micha@fragmental.art>
Date: Thu, 22 Aug 2024 08:31:14 +0200
Subject: [PATCH] coq: add another typing example

---
 coq/typing.v | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)

diff --git a/coq/typing.v b/coq/typing.v
index d11de58..595adcd 100644
--- a/coq/typing.v
+++ b/coq/typing.v
@@ -190,4 +190,23 @@ Proof.
   apply TSubst_VarReplace.
 Qed.
 
+
+Example typing4 : (is_well_typed
+  [[ Λ"T" ↦ Λ"U" ↦ λ"x" %"T"% ↦ λ"y" %"U"% ↦ %"x"% ]]
+).
+Proof.
+  unfold is_well_typed.
+  exists (ctx_assign "x" [%"T"%]
+            (ctx_assign "y" [%"U"%] ctx_empty)).
+  exists [ ∀"T",∀"U",%"T"%->%"U"%->%"T"% ].
+  apply T_CompatTypeAbs.
+  apply T_CompatTypeAbs.
+  apply T_CompatAbs.
+  apply C_take.
+  apply T_CompatAbs.
+  apply C_shuffle. apply C_take.
+  apply T_CompatVar.
+  apply C_take.
+Qed.
+
 End Typing.