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

diff --git a/matita/matita/lib/basics/logic.ma b/matita/matita/lib/basics/logic.ma
index 261cd77a8..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.
@@ -227,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.