From d1ec2de69c8975d1d253455d0ff892241d601d75 Mon Sep 17 00:00:00 2001 From: acciavat Date: Thu, 12 Oct 2006 09:53:08 +0000 Subject: [PATCH] auto => auto new. There is still one auto left that does not work with the new implementation (because of implicative hypothesis for local lemmas?) --- matita/contribs/CoRN/algebra/Setoids.ma | 9 ++------- 1 file changed, 2 insertions(+), 7 deletions(-) diff --git a/matita/contribs/CoRN/algebra/Setoids.ma b/matita/contribs/CoRN/algebra/Setoids.ma index 4fcb5a23b..6b7bf781d 100644 --- a/matita/contribs/CoRN/algebra/Setoids.ma +++ b/matita/contribs/CoRN/algebra/Setoids.ma @@ -1227,11 +1227,6 @@ qed. -axiom proper_caseZ_diff_CS : \forall CS : CSetoid. \forall f : nat \to nat \to CS. - (\forall m,n,p,q : nat. eq nat (plus m q) (plus n p) \to (f m n) = (f p q)) \to - \forall m,n : nat. caseZ_diff CS (Zminus (Z_of_nat m) (Z_of_nat n)) f = (f m n). - -(* lemma proper_caseZ_diff_CS : \forall CS : CSetoid. \forall f : nat \to nat \to CS. (\forall m,n,p,q : nat. eq nat (plus m q) (plus n p) \to (f m n) = (f p q)) \to \forall m,n : nat. caseZ_diff CS (Zminus (Z_of_nat m) (Z_of_nat n)) f = (f m n). @@ -1253,9 +1248,9 @@ apply f. apply n1. apply m1. apply eq_symmetric_unfolded.assumption. apply eq_symmetric_unfolded.assumption. apply H. -auto. +auto new. qed. -*) + (* Finally, we characterize functions defined on the natural numbers also as setoid functions, similarly to what we already did for predicates. *) -- 2.39.2