X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Ftechnicalities%2Fsetoids.ma;h=362b9fb5b740abc924761aa1159b3ebbb12ad640;hb=cf4088e2cabcbce9b112f1e1fd5cfd38fe16d427;hp=e589a33d047e65a16aa02e5a47469ecd193fe022;hpb=ccd879c23e341fe287f8fd1078c4cef459cf24f5;p=helm.git

diff --git a/helm/software/matita/library/technicalities/setoids.ma b/helm/software/matita/library/technicalities/setoids.ma
index e589a33d0..362b9fb5b 100644
--- a/helm/software/matita/library/technicalities/setoids.ma
+++ b/helm/software/matita/library/technicalities/setoids.ma
@@ -62,19 +62,19 @@ definition relation_class_of_argument_class : Argument_Class → Relation_Class.
 qed.
 
 definition carrier_of_relation_class : ∀X. X_Relation_Class X → Type.
- intros (X x); cases x; clear x; [2,4:clear x1] clear X; assumption.
+ intros (X x); cases x (A o o o o A o o A o o o A o A); exact A.
 qed.
 
 definition relation_of_relation_class:
  ∀X,R. carrier_of_relation_class X R → carrier_of_relation_class X R → Prop.
- intros 2; cases R; simplify; [1,2,3,4: assumption | apply (eq T) ]
+intros 2; cases R; simplify; [1,2,3,4: assumption | apply (eq T) ]
 qed.
 
 lemma about_carrier_of_relation_class_and_relation_class_of_argument_class :
  ∀R.
   carrier_of_relation_class ? (relation_class_of_argument_class R) =
    carrier_of_relation_class ? R.
- intro; cases R; reflexivity.
+intro; cases R; reflexivity.
 qed.
 
 inductive nelistT (A : Type) : Type :=
@@ -155,9 +155,7 @@ definition morphism_theory_of_function :
   generalize in match f; clear f;
   elim In;
    [ unfold make_compatibility_goal;
-     simplify;
-     intros;
-     whd;
+     whd; intros;
      reflexivity
    | simplify;
      intro;
@@ -530,7 +528,7 @@ qed.
 
 definition get_rewrite_direction: rewrite_direction → Argument_Class → rewrite_direction.
  intros (dir R);
- cases (variance_of_argument_class R);
+ cases (variance_of_argument_class R) (a);
   [ exact dir
   | cases a;
      [ exact dir                      (* covariant *)
@@ -569,12 +567,12 @@ definition relation_of_product_of_arguments:
   | intros;
     change in p with (Prod (carrier_of_relation_class variance t) (product_of_arguments n));
     change in p1 with (Prod (carrier_of_relation_class variance t) (product_of_arguments n));
-    cases p;
-    cases p1;
+    cases p (c p2);
+    cases p1 (c1 p3);
    apply And;
     [ exact
-      (directed_relation_of_argument_class (get_rewrite_direction r t) t a a1)
-    | exact (R b b1)
+      (directed_relation_of_argument_class (get_rewrite_direction r t) t c c1)
+    | exact (R p2 p3)
     ]
   ]
 qed. 
@@ -612,26 +610,21 @@ theorem apply_morphism_compatibility_Right2Left:
      generalize in match args1; clear args1;
      generalize in match m2; clear m2;
      generalize in match m1; clear m1;
-     elim t 0;
+     elim t 0; simplify;
       [ intros (T1 r Hs Hr m1 m2 args1 args2 H H1);
-        simplify in H;
-        simplify in H1;
-        simplify;
         apply H;
         exact H1
       | intros 8 (v T1 r Hr m1 m2 args1 args2);
-        cases v;
+        cases v; 
+        simplify;
         intros (H H1);
-        simplify in H1;
-        apply H;
-        exact H1
+        apply (H ? ? H1);
       | intros;
         apply H1;
         exact H2
       | intros 7 (v);
-        cases v;
+        cases v; simplify;
         intros (H H1);
-        simplify in H1;
         apply H;
         exact H1
       | intros;
@@ -726,10 +719,9 @@ theorem apply_morphism_compatibility_Left2Right:
         directed_relation_of_relation_class Left2Right ?
          (apply_morphism ? ? m1 args1)
          (apply_morphism ? ? m2 args2).
-  intro;
-  elim In;
-   [ simplify in m1 m2 args1 args2 ⊢ %;
-     change in H1 with
+  intro; 
+  elim In 0; simplify; intros;
+   [ change in H1 with
       (directed_relation_of_argument_class
         (get_rewrite_direction Left2Right t) t args1 args2);
      generalize in match H1; clear H1;
@@ -738,11 +730,8 @@ theorem apply_morphism_compatibility_Left2Right:
      generalize in match args1; clear args1;
      generalize in match m2; clear m2;
      generalize in match m1; clear m1;
-     elim t 0;
+     elim t 0; simplify;
       [ intros (T1 r Hs Hr m1 m2 args1 args2 H H1);
-        simplify in H;
-        simplify in H1;
-        simplify;
         apply H;
         exact H1
       | intros 8 (v T1 r Hr m1 m2 args1 args2);
@@ -793,7 +782,6 @@ theorem apply_morphism_compatibility_Left2Right:
      generalize in match m1; clear m1;
      elim t 0;
       [ intros (T1 r Hs Hr m1 m2 H1 t1 t3 H3);
-        simplify in H3;
         change in H1 with
          (∀x1,x2:T1.r x1 x2 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
      | intro v;