-inductive eq (C:Class) (c1:C): C \to Prop \def
- | eq_refl: cin ? c1 \to eq ? c1 c1
- | eq_sing_r: \forall c2,c3.
- eq ? c1 c2 \to cin ? c3 \to csub1 ? c2 c3 \to eq ? c1 c3
- | eq_sing_l: \forall c2,c3.
- eq ? c1 c2 \to cin ? c3 \to csub1 ? c3 c2 \to eq ? c1 c3.
-
-theorem eq_cl: \forall C,c1,c2. eq ? c1 c2 \to cin C c1 \land cin C c2.
-intros; elim H; clear H; clear c2;
- [ auto | decompose H2; auto | decompose H2; auto ].
-qed.
-
-theorem eq_trans: \forall C,c2,c1,c3.
- eq C c2 c3 \to eq ? c1 c2 \to eq ? c1 c3.
-intros 5; elim H; clear H; clear c3;
- [ auto
- | apply eq_sing_r; [||| apply H4 ]; auto
- | apply eq_sing_l; [||| apply H4 ]; auto
- ].
-qed.
-
-theorem eq_conf_rev: \forall C,c2,c1,c3.
- eq C c3 c2 \to eq ? c1 c2 \to eq ? c1 c3.
-intros 5; elim H; clear H; clear c2;
- [ auto
- | lapply eq_cl; [ decompose Hletin |||| apply H1 ].
- apply H2; apply eq_sing_l; [||| apply H4 ]; auto
- | lapply eq_cl; [ decompose Hletin |||| apply H1 ].
- apply H2; apply eq_sing_r; [||| apply H4 ]; auto
- ].
-qed.
-
-theorem eq_sym: \forall C,c1,c2. eq C c1 c2 \to eq C c2 c1.
-intros;
-lapply eq_cl; [ decompose Hletin |||| apply H ].
-auto.
-qed.
-
-theorem eq_conf: \forall C,c2,c1,c3.
- eq C c1 c2 \to eq ? c1 c3 \to eq ? c2 c3.
-intros.
-lapply eq_sym; [|||| apply H ].
-apply eq_trans; [| auto | auto ].
-qed.
+inductive ceq (C:Class) (c1:C): C \to Prop \def
+ | ceq_refl: cin ? c1 \to ceq ? c1 c1
+ | ceq_sing_r: \forall c2,c3.
+ ceq ? c1 c2 \to cin ? c3 \to cle1 ? c2 c3 \to ceq ? c1 c3
+ | ceq_sing_l: \forall c2,c3.
+ ceq ? c1 c2 \to cin ? c3 \to cle1 ? c3 c2 \to ceq ? c1 c3.