1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/PREDICATIVE-TOPOLOGY/class_eq".
17 include "class_defs.ma".
19 theorem ceq_cl: \forall C,c1,c2. ceq ? c1 c2 \to cin C c1 \land cin C c2.
20 intros; elim H; clear H; clear c2;
21 [ auto | decompose H2; auto | decompose H2; auto ].
24 theorem ceq_trans: \forall C,c2,c1,c3.
25 ceq C c2 c3 \to ceq ? c1 c2 \to ceq ? c1 c3.
26 intros 5; elim H; clear H; clear c3;
28 | apply ceq_sing_r; [||| apply H4 ]; auto
29 | apply ceq_sing_l; [||| apply H4 ]; auto
33 theorem ceq_conf_rev: \forall C,c2,c1,c3.
34 ceq C c3 c2 \to ceq ? c1 c2 \to ceq ? c1 c3.
35 intros 5; elim H; clear H; clear c2;
37 | lapply ceq_cl; [ decompose Hletin |||| apply H1 ].
38 apply H2; apply ceq_sing_l; [||| apply H4 ]; auto
39 | lapply ceq_cl; [ decompose Hletin |||| apply H1 ].
40 apply H2; apply ceq_sing_r; [||| apply H4 ]; auto
44 theorem ceq_sym: \forall C,c1,c2. ceq C c1 c2 \to ceq C c2 c1.
46 lapply ceq_cl; [ decompose Hletin |||| apply H ].
50 theorem ceq_conf: \forall C,c2,c1,c3.
51 ceq C c1 c2 \to ceq ? c1 c3 \to ceq ? c2 c3.
53 lapply ceq_sym; [|||| apply H ].
54 apply ceq_trans; [| auto | auto ].