-ndefinition R3 :
- ∀T0:Type[0].
- ∀a0:T0.
- ∀T1:∀x0:T0. a0=x0 → Type[0].
- ∀a1:T1 a0 (refl ? a0).
- ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ? a0 ? a1 ? p0 = x1 → Type[0].
- ∀a2:T2 a0 (refl ? a0) a1 (refl ? a1).
- ∀T3:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0.∀p1:R1 ? a0 ? a1 ? p0 = x1.
- ∀x2:T2 x0 p0 x1 p1.R2 ? a0 ? a1 ? ? p0 ? p1 a2 = x2 → Type[0].
- ∀b0:T0.
- ∀e0:a0 = b0.
- ∀b1: T1 b0 e0.
- ∀e1:R1 ? a0 ? a1 ? e0 = b1.
- ∀b2: T2 b0 e0 b1 e1.
- ∀e2:R2 ? a0 ? a1 ? ? e0 ? e1 a2 = b2.
- ∀so:T3 a0 (refl ? a0) a1 (refl ? a1) a2 (refl ? a2).T3 b0 e0 b1 e1 b2 e2.
-#T0;#a0;#T1;#a1;#T2;#a2;#T3;#b0;#e0;#b1;#e1;#b2;#e2;#H;
-napply (eq_rect_Type0 ????? e2);
-napply (R2 ?? ? ??? e0 ? e1);
-napply H;
+(* nlemma prova : ∀T:Type[0].∀a,b:T.∀e:a = b.
+ ∀P:∀x,y:T.x=y→Prop.P a a (refl T a) → P a b e.
+#T;#a;#b;#e;#P;#H;
+nrewrite < e;*)
+
+ninductive I1 : Type[0] ≝
+| k1 : I1.
+
+ninductive I2 : I1 → Type[0] ≝
+| k2 : ∀x.I2 x.
+
+ninductive I3 : ∀x:I1.I2 x → Type[0] ≝
+| k3 : ∀x,y.I3 x y.
+
+ninductive I4 : ∀x,y.I3 x y → Type[0] ≝
+| k4 : ∀x,y.∀z:I3 x y.I4 x y z.
+
+(*alias id "eq" = "cic:/matita/ng/logic/equality/eq.ind(1,0,2)".
+alias id "refl" = "cic:/matita/ng/logic/equality/eq.con(0,1,2)".*)
+
+ninductive II : Type[0] ≝
+| kII1 : ∀x,y,z.∀w:I4 x y z.II
+| kII2 : ∀x,y,z.∀w:I4 x y z.II.
+
+(* nlemma foo : ∀a,b,c,d,e,f,g,h. kII1 a b c d = kII2 e f g h → True.
+#a;#b;#c;#d;#e;#f;#g;#h;#H;
+ndiscriminate H;
+nqed. *)
+
+nlemma faof : ∀a,b,c,d,e,f,g,h.∀Heq:kII1 a b c d = kII1 e f g h.
+ ∀P:(∀a,b,c,d.kII1 a b c d = kII1 e f g h → Prop).
+ P e f g h (refl ??) → P a b c d Heq.
+#a;#b;#c;#d;#e;#f;#g;#h;#Heq;#P;#HP;
+ndestruct;
+napply HP;