X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Fbasics%2Feq.ma;h=4a29e2843a7103873530343383781682866abb0d;hb=e678e3b1a88e657401902bbddad02d3a4d70205a;hp=56a73337875ff61096493a49214604a85f552f74;hpb=adc7a41ccbed2f36778c662d8a2ce06e192fb555;p=helm.git

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