proposition: Lemma equiv_clot_Kl: union_K_equiv (eqv_clot h) =2 eqv_clot union_K_pairs.
proof: Proof. move=> x y. rewrite /union_K_equiv map_equivE. rewrite !eqv_clotE. set e1 := rel_of_pairs _. set e2 := rel_of_pairs _. apply/idP/idP. - suff S u v : equiv_of e1 u v -> equiv_of e2 (sum_left k u) (sum_left k v) by apply: S. apply: equiv_ofE => {u v} [[u|u] [u'|u']] /= H. all: rewrite /e2 /sum_left; apply: sub_equiv_of; apply/mapP. + by exists (unl u,unl u'). + by exists (unl u,unr u'). + by exists (unr u,unl u'). + by exists (unr u,unr u'). - apply: equiv_ofE => {x y} x x' xx'. have kh' z : equiv_of e1 (unr z) (unl (k z)). { rewrite -eqv_clotE. apply/eqquotP. exact: kh. } case/mapP : xx' => [[[u|u] [v|v]] H] /= [-> ->] {x x'}. + exact: sub_equiv_of. + etransitivity. 2: apply kh'. by apply sub_equiv_of. + etransitivity. symmetry; apply kh'. by apply sub_equiv_of. + etransitivity. 2: apply kh'. etransitivity. symmetry; apply kh'. by apply sub_equiv_of. Qed.
imports: Coq(Morphisms RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij) GraphTheory(equiv digraph setoid_bigop structures)