- character: we adjusted some "autobatch" parameters

[helm.git] / helm / software / matita / contribs / limits / Class / eq.ma

diff --git a/helm/software/matita/contribs/limits/Class/eq.ma b/helm/software/matita/contribs/limits/Class/eq.ma
index 69d6836d8159b0ef0f7b50b82a0ca0e121d44344..003365bf4a59408f6eef5feeb1402f9e133cc633 100644 (file)
--- 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.