X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Fcontribs%2FPREDICATIVE-TOPOLOGY%2Fclass_eq.ma;h=cfcb57293f6a066eced2e45621d9387398db64b9;hb=112afe13b5aef27425d1a0bc9c71a70b491069bf;hp=5c53b94596d2be574982d277f33bcd799196239e;hpb=e3ba094ac1ba1f73fbb558944715cfa6707da868;p=helm.git

diff --git a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/class_eq.ma b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/class_eq.ma
index 5c53b9459..cfcb57293 100644
--- a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/class_eq.ma
+++ b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/class_eq.ma
@@ -14,42 +14,25 @@
 
 set "baseuri" "cic:/matita/PREDICATIVE-TOPOLOGY/class_eq".
 
-include "class_defs.ma".
+include "class_le.ma".
 
 theorem ceq_cl: \forall C,c1,c2. ceq ? c1 c2 \to cin C c1 \land cin C c2.
-intros; elim H; clear H; clear c2; 
-   [ auto | decompose H2; auto | decompose H2; auto ].
+intros; elim H; clear H.
+lapply cle_cl to H1 using H; clear H1; decompose H;
+lapply cle_cl to H2 using H; clear H2; decompose H.
+auto.
 qed.
 
-theorem ceq_trans: \forall C,c2,c1,c3.
-                   ceq C c2 c3 \to ceq ? c1 c2 \to ceq ? c1 c3.
-intros 5; elim H; clear H; clear c3;
-   [ auto 
-   | apply ceq_sing_r; [||| apply H4 ]; auto
-   | apply ceq_sing_l; [||| apply H4 ]; auto
-   ].
+theorem ceq_refl: \forall C,c. cin C c \to ceq ? c c.
+intros; apply ceq_intro; auto.
 qed.
 
-theorem ceq_conf_rev: \forall C,c2,c1,c3.
-                      ceq C c3 c2 \to ceq ? c1 c2 \to ceq ? c1 c3.
-intros 5; elim H; clear H; clear c2;
-   [ auto 
-   | lapply ceq_cl; [ decompose Hletin |||| apply H1 ].
-     apply H2; apply ceq_sing_l; [||| apply H4 ]; auto
-   | lapply ceq_cl; [ decompose Hletin |||| apply H1 ].
-     apply H2; apply ceq_sing_r; [||| apply H4 ]; auto
-   ].
+theorem ceq_trans: \forall C,c2,c1,c3.
+                   ceq C c2 c3 \to ceq ? c1 c2 \to ceq ? c1 c3.
+intros; elim H; elim H1; clear H; clear H1.
+apply ceq_intro; apply cle_trans; [|auto|auto||auto|auto].
 qed.
 
 theorem ceq_sym: \forall C,c1,c2. ceq C c1 c2 \to ceq C c2 c1.
-intros;
-lapply ceq_cl; [ decompose Hletin |||| apply H ].
-auto.
-qed.
-
-theorem ceq_conf: \forall C,c2,c1,c3.
-                  ceq C c1 c2 \to ceq ? c1 c3 \to ceq ? c2 c3.
-intros.
-lapply ceq_sym; [|||| apply H ].
-apply ceq_trans; [| auto | auto ].
+intros; elim H; clear H.; auto.
 qed.