Automatic generation of elimination and inversion principles for co-inductive

[helm.git] / helm / software / matita / library / technicalities / setoids.ma

diff --git a/helm/software/matita/library/technicalities/setoids.ma b/helm/software/matita/library/technicalities/setoids.ma
index b945931c14dab117679f714a0a3c3d7e3aa1cd72..f9c5e878bf1490346d82810827c2aea0d9470f36 100644 (file)
--- a/helm/software/matita/library/technicalities/setoids.ma
+++ b/helm/software/matita/library/technicalities/setoids.ma
@@ -18,8 +18,8 @@
 set "baseuri" "cic:/matita/technicalities/setoids".
 
 include "datatypes/constructors.ma".
-include "logic/connectives2.ma".
 include "logic/coimplication.ma".
+include "logic/connectives2.ma".
 
 (* DEFINITIONS OF Relation_Class AND n-ARY Morphism_Theory *)
 
@@ -150,8 +150,8 @@ definition morphism_theory_of_function :
     Morphism_Theory In' Out'.
   intros;
   apply (mk_Morphism_Theory ? ? f);
-  unfold In' in f; clear In';
-  unfold Out' in f; clear Out';
+  unfold In' in f ⊢ %; clear In';
+  unfold Out' in f ⊢ %; clear Out';
   generalize in match f; clear f;
   elim In;
    [ unfold make_compatibility_goal;
@@ -203,7 +203,7 @@ definition equality_morphism_of_symmetric_areflexive_transitive_relation:
  apply mk_Morphism_Theory;
   [ exact Aeq
   | unfold make_compatibility_goal;
-    simplify;
+    simplify; unfold ASetoidClass; simplify;
     intros;
     split;
     unfold transitive in H;
@@ -236,7 +236,7 @@ definition equality_morphism_of_symmetric_reflexive_transitive_relation:
     (Morphism_Theory (cons ? ASetoidClass (singl ? ASetoidClass)) Iff_Relation_Class).
  intros;
  apply mk_Morphism_Theory;
- reduce;
+ normalize;
   [ exact Aeq
   | intros;
     split;
@@ -275,7 +275,7 @@ definition equality_morphism_of_asymmetric_areflexive_transitive_relation:
  apply mk_Morphism_Theory;
  [ simplify;
    apply Aeq
- | simplify;
+ | simplify; unfold ASetoidClass1; simplify; unfold ASetoidClass2; simplify;
    intros;
    whd;
    intros;
@@ -298,7 +298,7 @@ definition equality_morphism_of_asymmetric_reflexive_transitive_relation:
  apply mk_Morphism_Theory;
  [ simplify;
    apply Aeq
- | simplify;
+ | simplify; unfold ASetoidClass1; simplify; unfold ASetoidClass2; simplify;
    intros;
    whd;
    intro;
@@ -332,7 +332,7 @@ definition morphism_theory_of_predicate :
   | generalize in match f; clear f;
     unfold In'; clear In';
     elim In;
-     [ reduce;
+     [ normalize;
        intro;
        apply iff_refl
      | simplify;