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.