∀A.∀a.∀P: ∀x:A. x = a → Prop. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
#A #a #P #p #x0 #p0; @(eq_rect_r ? ? ? p0) //; qed.
+lemma eq_rect_Type0_r:
+ ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
+ #A #a #P #H #x #p (generalize in match H) (generalize in match P)
+ cases p; //; qed.
+
lemma eq_rect_Type2_r:
∀A.∀a.∀P: ∀x:A. eq ? x a → Type[2]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
#A #a #P #H #x #p (generalize in match H) (generalize in match P)
∀x1,x2:A.∀y1,y2:B. x1=x2 → y1=y2 → f x1 y1 = f x2 y2.
#A #B #C #f #x1 #x2 #y1 #y2 #E1 #E2 >E1; >E2; //; qed.
+lemma eq_f3: ∀A,B,C,D.∀f:A→B→C->D.
+∀x1,x2:A.∀y1,y2:B. ∀z1,z2:C. x1=x2 → y1=y2 → z1=z2 → f x1 y1 z1 = f x2 y2 z2.
+#A #B #C #D #f #x1 #x2 #y1 #y2 #z1 #z2 #E1 #E2 #E3 >E1; >E2; >E3 //; qed.
+
(* hint to genereric equality
definition eq_equality: equality ≝
mk_equality eq refl rewrite_l rewrite_r.
definition R1 ≝ eq_rect_Type0.
-(*
+(* used for lambda-delta *)
definition R2 :
∀T0:Type[0].
∀a0:T0.
∀b1: T1 b0 e0.
∀e1:R1 ?? T1 a1 ? e0 = b1.
T2 b0 e0 b1 e1.
-#T0;#a0;#T1;#a1;#T2;#a2;#b0;#e0;#b1;#e1;
-napply (eq_rect_Type0 ????? e1);
-napply (R1 ?? ? ?? e0);
-napply a2;
-nqed.
+#T0 #a0 #T1 #a1 #T2 #a2 #b0 #e0 #b1 #e1
+@(eq_rect_Type0 ????? e1)
+@(R1 ?? ? ?? e0)
+@a2
+qed.
-ndefinition R3 :
+definition R3 :
∀T0:Type[0].
∀a0:T0.
∀T1:∀x0:T0. a0=x0 → Type[0].
∀b2: T2 b0 e0 b1 e1.
∀e2:R2 ???? T2 a2 b0 e0 ? e1 = b2.
T3 b0 e0 b1 e1 b2 e2.
-#T0;#a0;#T1;#a1;#T2;#a2;#T3;#a3;#b0;#e0;#b1;#e1;#b2;#e2;
-napply (eq_rect_Type0 ????? e2);
-napply (R2 ?? ? ???? e0 ? e1);
-napply a3;
-nqed.
+#T0 #a0 #T1 #a1 #T2 #a2 #T3 #a3 #b0 #e0 #b1 #e1 #b2 #e2
+@(eq_rect_Type0 ????? e2)
+@(R2 ?? ? ???? e0 ? e1)
+@a3
+qed.
-ndefinition R4 :
+definition R4 :
∀T0:Type[0].
∀a0:T0.
∀T1:∀x0:T0. eq T0 a0 x0 → Type[0].
∀b3: T3 b0 e0 b1 e1 b2 e2.
∀e3:eq (T3 …) (R3 T0 a0 T1 a1 T2 a2 T3 a3 b0 e0 b1 e1 b2 e2) b3.
T4 b0 e0 b1 e1 b2 e2 b3 e3.
-#T0;#a0;#T1;#a1;#T2;#a2;#T3;#a3;#T4;#a4;#b0;#e0;#b1;#e1;#b2;#e2;#b3;#e3;
-napply (eq_rect_Type0 ????? e3);
-napply (R3 ????????? e0 ? e1 ? e2);
-napply a4;
-nqed.
-
-naxiom streicherK : ∀T:Type[2].∀t:T.∀P:t = t → Type[2].P (refl ? t) → ∀p.P p. *)
+#T0 #a0 #T1 #a1 #T2 #a2 #T3 #a3 #T4 #a4 #b0 #e0 #b1 #e1 #b2 #e2 #b3 #e3
+@(eq_rect_Type0 ????? e3)
+@(R3 ????????? e0 ? e1 ? e2)
+@a4
+qed.
+
+(* TODO concrete definition by means of proof irrelevance *)
+axiom streicherK : ∀T:Type[1].∀t:T.∀P:t = t → Type[2].P (refl ? t) → ∀p.P p.