proposition: Lemma union_equiv_l_class: equiv_class_of union_equiv_l_rel.
proof: Proof. split => [[x|x]|[x|x] [y|y]|[x|x] [y|y] [z|z]]//=. apply: equiv_sym. apply: equiv_trans. by move=>/eqP ->. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries bij)