From 92b9fb7c477eb1b0dbf5d921555d9a0295d0e46d Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Thu, 28 Apr 2011 15:24:48 +0000
Subject: [PATCH] we uncommented R3 and R4 tu be used in lambda-delta

---
 matita/matita/lib/basics/logic.ma | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

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.
-- 
2.39.2