proposition: Lemma exercise6_5 (x := C3) (g1:= special_equivalence C0 C1 x) (g2:= special_equivalence C0 C2 x): [/\ equivalence g1, equivalence g2, substrate g1 = x, substrate g2 = x & ~ (equivalence (g1 \cup g2))].
proof: Proof. split. apply: special_equivalence_ea; apply /C3_P; in_TP4. apply: special_equivalence_ea; apply /C3_P; in_TP4. rewrite substrate_special_equivalence //; apply /C3_P; in_TP4. rewrite substrate_special_equivalence //; apply /C3_P; in_TP4. move=> bad. have p1: (related (g1 \cup g2) C1 C0). apply /setU2_P; left;apply/setU2_P; left; fprops. have p2: (related (g1 \cup g2) C0 C2). apply /setU2_P; right;apply/setU2_P; left; fprops. have :(related (g1 \cup g2) C1 C2) by equiv_tac. move: C2_ne_C01 => [n1 n2]. case /setU2_P; case/setU2_P. by case/set2_P=> eq2; move: (pr2_def eq2); auto. by move /diagonal_pi_P => [_]; auto. by case/set2_P=> eq2; move: (pr1_def eq2); fprops. by move /diagonal_pi_P => [_]; auto. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)