-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.