From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Tue, 23 Mar 2010 16:31:55 +0000 (+0000)
Subject: Readded eqf_2.
X-Git-Tag: make_still_working~2978
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=356f4b5b71fc1919a10a0caee28be49412b2af71;p=helm.git

Readded eqf_2.

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>
---

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