∀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.
-(* useless stuff
+(* used for lambda-delta *)
definition R2 :
∀T0:Type[0].
∀a0:T0.
@(eq_rect_Type0 ????? e3)
@(R3 ????????? e0 ? e1 ? e2)
@a4
-qed. *)
+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.