refl: eq A x x.
interpretation "leibnitz's equality" 'eq t x y = (eq t x y).
+interpretation "leibniz reflexivity" 'refl = refl.
lemma eq_rect_r:
∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → Type[2]. P a (refl A a) → P x p.
∀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.
-(* 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.
+definition eqProp ≝ λA:Prop.eq A.
+
+(* Example to avoid indexing and the consequential creation of ill typed
+ terms during paramodulation *)
+example lemmaK : ∀A.∀x:A.∀h:x=x. eqProp ? h (refl A x).
+#A #x #h @(refl ? h: eqProp ? ? ?).
+qed.
+
+theorem streicherK : ∀T:Type[1].∀t:T.∀P:t = t → Type[2].P (refl ? t) → ∀p.P p.
+ #T #t #P #H #p >(lemmaK ?? p) @H
+qed.