proposition: Lemma finer_sub_equivP: (finer_equivalence s r <-> sub s r).
proof: Proof. move: fa => [es er srss]. split. move=> fe t ts. have gs: (sgraph s) by fprops. by rewrite -(gs _ ts); apply: fe; hnf; rewrite (gs _ ts). move => t x y; rewrite /related; apply: t. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)