From: Andrea Asperti 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 --- 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