X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fbasics%2Flogic.ma;h=70e743e993ac96c12cdbf7a4a56cdc23bc8280b6;hb=6756545478920d6eca9445a3aeede39bfe11cb83;hp=8f981d46924556ee885407a1320d147ef07aaad0;hpb=2225846a2ee76026bef7c3e8eacc42e86c3ae6a2;p=helm.git

diff --git a/matita/matita/lib/basics/logic.ma b/matita/matita/lib/basics/logic.ma
index 8f981d469..70e743e99 100644
--- a/matita/matita/lib/basics/logic.ma
+++ b/matita/matita/lib/basics/logic.ma
@@ -263,10 +263,10 @@ 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).
+lemma lemmaK : ∀A.∀x:A.∀h:x=x. eqProp ? h (refl A x).
 #A #x #h @(refl ? h: eqProp ? ? ?).
-qed.
+qed-.
 
 theorem streicherK : ∀T:Type[2].∀t:T.∀P:t = t → Type[3].P (refl ? t) → ∀p.P p.
  #T #t #P #H #p >(lemmaK T t p) @H
-qed.
+qed-.