+(* lemma idfof : (∀t1,t2,t3,u1,u2,u3.((λy1:ℕ.λp1:t1=y1.λy2:I1 y1.λp2:R1 ℕ t1 (λy1:ℕ.λp1:t1=y1.I1 y1) t2 y1 p1 =y2.
+ λy3:I2 y1 y2.λp3:R2 ℕ t1 (λy1:ℕ.λp1:t1=y1.I1 y1) t2 (λy1:ℕ.λp1:t1=y1.λy2:I1 y1.λp2:R1 ℕ t1 (λy1:ℕ.λp1:t1 =y1.I1 y1) t2 y1 p1 =y2.I2 y1 y2) t3 y1 p1 y2 p2 =y3.
+ kI3 y1 y2 y3 =kI3 u1 u2 u3)
+t1 (refl_eq ℕ t1) t2 (refl_eq ((λy1:ℕ.λp1:t1=y1.I1 y1) t1 (refl_eq ℕ t1)) t2)
+ t3 (refl_eq ((λy1:ℕ.λp1:t1=y1.λy2:I1 y1.λp2:R1 ℕ t1 (λy1:ℕ.λp1:t1=y1.I1 y1) t2 y1 p1 =y2.I2 y1 y2) t1 (refl_eq ℕ t1) t2 (refl_eq ((λy1:ℕ.λp1:t1=y1.I1 y1) t1 (refl_eq ℕ t1)) t2)) t3)
+ )
+ → True).
+simplify; *)
+
+definition I3d : ∀x,y:I3.x = y → Type ≝
+λx,y.match x return (λx:I3.x = y → Type) with
+[ kI3 x1 x2 x3 ⇒ match y return (λy:I3.kI3 x1 x2 x3 = y → Type) with
+ [ kI3 y1 y2 y3 ⇒
+ λe:kI3 x1 x2 x3 = kI3 y1 y2 y3.
+ ∀P:Prop.(∀e1: x1 = y1.
+ ∀e2: R1 ?? (λz1,p1.I1 z1) ?? e1 = y2.
+ ∀e3: R2 ???? (λz1,p1,z2,p2.I2 z1 z2) x3 ? e1 ? e2 = y3.
+ R3 ??????
+ (λz1,p1,z2,p2,z3,p3.
+ eq ? (kI3 z1 z2 z3) (kI3 y1 y2 y3)) e y1 e1 y2 e2 y3 e3
+ = refl_eq ? (kI3 y1 y2 y3)
+ → P) → P]].
+
+definition I3d : ∀x,y:I3.x=y → Type.
+intros 2;cases x;cases y;intro;
+apply (∀P:Prop.(∀e1: x1 = x3.
+ ∀e2: R1 ?? (λy1,p1.I1 y1) ?? e1 = x4.
+ ∀e3: R2 ???? (λy1,p1,y2,p2.I2 y1 y2) i ? e1 ? e2 = i1.
+ R3 ??????
+ (λy1,p1,y2,p2,y3,p3.
+ eq ? (kI3 y1 y2 y3) (kI3 x3 x4 i1)) H x3 e1 x4 e2 i1 e3
+ = refl_eq ? (kI3 x3 x4 i1)
+ → P) → P);
+qed.
+
+(* definition I3d : ∀x,y:nat. x = y → Type ≝
+λx,y.
+match x
+ return (λx.x = y → Type)
+ with
+[ O ⇒ match y return (λy.O = y → Type) with
+ [ O ⇒ λe:O = O.∀P.P → P
+ | S q ⇒ λe: O = S q. ∀P.P]
+| S p ⇒ match y return (λy.S p = y → Type) with
+ [ O ⇒ λe:S p = O.∀P.P
+ | S q ⇒ λe: S p = S q. ∀P.(p = q → P) → P]].
+
+definition I3d:
+ ∀x,y:I3. x = y → Type
+ ≝
+λx,y.
+match x with
+[ kI3 t1 t2 (t3:I2 t1 t2) ⇒ match y with
+ [ kI3 u1 u2 u3 ⇒ λe:kI3 t1 t2 t3 = kI3 u1 u2 u3.∀P:Type.
+ (∀e1: t1 = u1.
+ ∀e2: R1 nat t1 (λy1:nat.λp1:y1 = u1.I1 y1) t2 ? e1 = u2.
+ ∀e3: R2 nat t1 (λy1,p1.I1 y1) t2 (λy1,p1,y2,p2.I2 y1 y2) t3 ? e1 ? e2 = u3.
+ (* ∀e: kI3 t1 t2 t3 = kI3 u1 u2 u3.*)
+ R3 nat t1 (λy1,p1.I1 y1) t2 (λy1,p1,y2,p2.I2 y1 y2) t3
+ (λy1,p1,y2,p2,y3,p3.eq I3 (kI3 y1 y2 y3) (kI3 u1 u2 u3)) e u1 e1 u2 e2 u3 e3 = refl_eq I3 (kI3 u1 u2 u3)
+ → P)
+ → P]].
+
+definition I3d:
+ ∀x,y:I3.
+ (∀x,y.match x with [ kI3 t1 t2 t3 ⇒
+ match y with [ kI3 u1 u2 u3 ⇒ kI3 t1 t2 t3 = kI3 u1 u2 u3]]) → Type
+ ≝
+λx,y.λe:
+ (∀x,y.match x with [ kI3 t1 t2 t3 ⇒
+ match y with [ kI3 u1 u2 u3 ⇒ kI3 t1 t2 t3 = kI3 u1 u2 u3]]).
+match x with