proposition: Lemma special_equivalence_ea a b x: inc a x -> inc b x -> equivalence(special_equivalence a b x).
proof: Proof. move=> ax bx. have gs: sgraph (special_equivalence a b x). move=> t; move/setU2_P; case; first by case/set2_P => ->; fprops. by move /diagonal_i_P => []. have pair_symm: forall a b c d, J a b = J c d -> J b a = J d c. move=> u v u' v' eql. apply: pair_exten; fprops; aw. apply: (pr2_def eql). apply: (pr1_def eql). apply: symmetric_transitive_equivalence => //. move=> u v h; case/setU2_P: (h). case /set2_P => ww; apply/setU2_P; left; rewrite (pr1_def ww)(pr2_def ww); fprops. by move => /diagonal_pi_P [_ uv]; move: h;rewrite uv. move=> u v w ra rb. case /setU2_P: (ra); last by move => /diagonal_pi_P [_ ->]. case /setU2_P: (rb); last by move => /diagonal_pi_P [_ <-]. move => h1 h2; apply/setU2_P. case /set2_P: h1 => h11; rewrite (pr2_def h11); case /set2_P: h2 => h22; rewrite (pr1_def h22). - left; fprops. - by right; apply /diagonal_pi_P. - by right; apply /diagonal_pi_P. - left; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)