X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fbasics%2Flogic.ma;h=b090a8de8fc80136a2b6523ce8cc6b6cad09dd30;hb=78f21d7d9014e5c7655f58239e4f1a128ea2c558;hp=0754d7afc147ee1c806ccafe9fa3c2a92bdaf0c1;hpb=95bb2b7593bf67b7a0758a63631a394af22dfae5;p=helm.git

diff --git a/matita/matita/lib/basics/logic.ma b/matita/matita/lib/basics/logic.ma
index 0754d7afc..b090a8de8 100644
--- a/matita/matita/lib/basics/logic.ma
+++ b/matita/matita/lib/basics/logic.ma
@@ -18,6 +18,7 @@ inductive eq (A:Type[1]) (x:A) : A → Prop ≝
     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.
@@ -27,6 +28,11 @@ lemma eq_ind_r :
  ∀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)
@@ -55,6 +61,10 @@ theorem eq_f2: ∀A,B,C.∀f:A→B→C.
 ∀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.
@@ -141,7 +151,7 @@ definition R0 ≝ λT:Type[0].λt:T.t.
   
 definition R1 ≝ eq_rect_Type0.
 
-
+(* used for lambda-delta *)
 definition R2 :
   ∀T0:Type[0].
   ∀a0:T0.
@@ -218,5 +228,14 @@ definition R4 :
 @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.
+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.