X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fbasics%2Flogic.ma;h=32124c2fbaaad21eb038bbb6d0e31e3feb70248e;hb=42680d47c033d751738fd0f84af7b45b2a91a5b8;hp=1b801a14bf8f339ef9fd20ff57072edd1022d595;hpb=6bbf27282bad84e066bb952e41dbc8f72b31de6c;p=helm.git

diff --git a/matita/matita/lib/basics/logic.ma b/matita/matita/lib/basics/logic.ma
index 1b801a14b..32124c2fb 100644
--- a/matita/matita/lib/basics/logic.ma
+++ b/matita/matita/lib/basics/logic.ma
@@ -141,7 +141,7 @@ definition R0 ≝ λT:Type[0].λt:T.t.
   
 definition R1 ≝ eq_rect_Type0.
 
-(* useless stuff
+(* used for lambda-delta *)
 definition R2 :
   ∀T0:Type[0].
   ∀a0:T0.
@@ -216,7 +216,7 @@ definition R4 :
 @(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.