proposition: Lemma sc_eq T T' (e : rel T) (e' : rel T') f x y : (forall x y, e' (f x) (f y) = e x y) -> sc e' (f x) (f y) = sc e x y.
proof: Proof. move => H. by rewrite /sc /= !H. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)