diff --git a/coq/equiv.v b/coq/equiv.v
index 630783f..09c735e 100644
--- a/coq/equiv.v
+++ b/coq/equiv.v
@@ -220,6 +220,16 @@ Inductive type_eq : type_term -> type_term -> Prop :=
     y === z ->
     x === z
 
+  | TEq_SubFun : forall x x' y y',
+    x === x' ->
+    y === y' ->
+    [< x -> y >] === [< x' -> y' >]
+
+  | TEq_SubMorph : forall x x' y y',
+    x === x' ->
+    y === y' ->
+    [< x ->morph y >] === [< x' ->morph y' >]
+
   | TEq_LadderAssocLR : forall x y z,
     [< (x~y)~z >]
     ===
@@ -259,7 +269,11 @@ Proof.
   apply TEq_Trans with (y:=y).
   apply IHtype_eq2.
   apply IHtype_eq1.
-  
+
+  apply TEq_SubFun.
+  auto. auto.
+  apply TEq_SubMorph.
+  auto. auto.
   apply TEq_LadderAssocRL.
   apply TEq_LadderAssocLR.