From 356f4b5b71fc1919a10a0caee28be49412b2af71 Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Tue, 23 Mar 2010 16:31:55 +0000
Subject: [PATCH] Readded eqf_2.

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>
---
 helm/software/matita/nlibrary/basics/eq.ma | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/helm/software/matita/nlibrary/basics/eq.ma b/helm/software/matita/nlibrary/basics/eq.ma
index 56a733378..4a29e2843 100644
--- a/helm/software/matita/nlibrary/basics/eq.ma
+++ b/helm/software/matita/nlibrary/basics/eq.ma
@@ -48,8 +48,8 @@ theorem eq_f': \forall  A,B:Type.\forall f:A\to B.
 intros.elim H.apply refl_eq.
 qed. *)
 
-(* deleterio per auto
+(* deleterio per auto*)
 ntheorem eq_f2: ∀A,B,C:Type.∀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; nrewrite > E1; nrewrite > E2;//.
-nqed. *)
\ No newline at end of file
+nqed. 
\ No newline at end of file
-- 
2.39.2