X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Flimits%2FClass%2Feq.ma;h=003365bf4a59408f6eef5feeb1402f9e133cc633;hb=cad56a7b9eadce5aef71c5b14192181a847dde27;hp=69d6836d8159b0ef0f7b50b82a0ca0e121d44344;hpb=700b170aa9b0377d33f1edd44de8d89129477fb8;p=helm.git

diff --git a/helm/software/matita/contribs/limits/Class/eq.ma b/helm/software/matita/contribs/limits/Class/eq.ma
index 69d6836d8..003365bf4 100644
--- a/helm/software/matita/contribs/limits/Class/eq.ma
+++ b/helm/software/matita/contribs/limits/Class/eq.ma
@@ -14,31 +14,31 @@
 
 include "Class/defs.ma".
 
-(* ACZEL CATEGORIES:
+(* CLASSES:
    - Here we prove the standard properties of the equality.
 *)
 
-theorem ceq_cin_sx: ∀C,c1,c2. ceq C c1 c2 → cin ? c1.
-intros; elim H; clear H c1 c2; autobatch.
+theorem ceq_cin_fw: ∀C,c1,c2. ceq C c1 c2 → cin ? c1 → cin ? c2.
+intros 4; elim H; clear H c1 c2; autobatch.
 qed.
 
-theorem ceq_cin_dx: ∀C,c1,c2. ceq C c1 c2 → cin ? c2.
-intros; elim H; clear H c1 c2; autobatch.
+theorem ceq_cin_bw: ∀C,c1,c2. ceq C c1 c2 → cin ? c2 → cin ? c1.
+intros 4; elim H; clear H c1 c2; autobatch.
 qed.
 
 theorem ceq_trans: ∀C,c1,c2. ceq C c1 c2 → ∀c3. ceq ? c2 c3 → ceq ? c1 c3.
 intros 4; elim H; clear H c1 c2; autobatch.
 qed.
 
-theorem ceq_conf: ∀C,c1,c2. ceq C c1 c2 → ∀c3. ceq ? c1 c3 → ceq ? c2 c3.
-intros 4; elim H; clear H c1 c2; autobatch depth = 4.
+theorem ceq_sym: ∀ C,c1,c2. ceq C c1 c2 → ceq ? c2 c1.
+intros; elim H; clear H c1 c2; autobatch.
 qed.
 
-theorem ceq_sym: ∀ C,c1,c2. ceq C c1 c2 → ceq ? c2 c1.
-intros; autobatch depth = 4.
+theorem ceq_conf: ∀C,c1,c2. ceq C c1 c2 → ∀c3. ceq ? c1 c3 → ceq ? c2 c3.
+intros; autobatch.
 qed.
 
 theorem ceq_repl: ∀C,c1,c2. ceq C c1 c2 →
-                      ∀d1. ceq ? c1 d1 → ∀d2. ceq ? c2 d2 → ceq ? d1 d2.
+                  ∀d1. ceq ? c1 d1 → ∀d2. ceq ? c2 d2 → ceq ? d1 d2.
 intros; autobatch.
 qed.