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.