Nuova dimostrazione riflessiva di le_to_Bertrand.

[helm.git] / helm / software / matita / library / algebra / CoRN / Setoids.ma

diff --git a/helm/software/matita/library/algebra/CoRN/Setoids.ma b/helm/software/matita/library/algebra/CoRN/Setoids.ma
index 30c8c8bd5d128ebefbfc2d212f5e7ac75f8927ac..ddbb807a85643681b923fc6ee91afb367b0d6c50 100644 (file)
--- a/helm/software/matita/library/algebra/CoRN/Setoids.ma
+++ b/helm/software/matita/library/algebra/CoRN/Setoids.ma
@@ -1115,7 +1115,7 @@ intros.
 unfold.unfold.intros 2.elim x 2.elim y 2.
 simplify.
 intro.
-reduce in H2.
+normalize in H2.
 apply (un_op_wd_unfolded ? f ? ? H2).
 qed.
 
@@ -1123,7 +1123,7 @@ lemma restr_un_op_strext : \forall S:CSetoid. \forall P: S \to Prop.
 \forall f: CSetoid_un_op S. \forall pr: un_op_pres_pred S P f.  
 un_op_strext (mk_SubCSetoid S P) (restr_un_op S P f pr).
 intros.unfold.unfold. intros 2.elim y 2. elim x 2.
-intros.reduce in H2.
+intros.normalize in H2.
 apply (cs_un_op_strext ? f ? ? H2).
 qed.
 
@@ -1182,8 +1182,8 @@ intros.
 unfold.unfold.intros 2.elim x1 2. elim x2 2.intros 2. elim y1 2. elim y2 2.
 simplify.
 intros.
-reduce in H4.
-reduce in H5.
+normalize in H4.
+normalize in H5.
 apply (cs_bin_op_wd ? f ? ? ? ? H4 H5).
 qed.
 
@@ -1192,7 +1192,7 @@ lemma restr_bin_op_strext : \forall S:CSetoid. \forall P: S \to Prop.
 bin_op_strext (mk_SubCSetoid S P) (restr_bin_op S P f pr).
 intros.unfold.unfold. intros 2.elim x1 2. elim x2 2.intros 2. elim y1 2. elim y2 2.
 simplify.intros.
-reduce in H4.
+normalize in H4.
 apply (cs_bin_op_strext ? f ? ? ? ? H4).
 qed.