proposition: Lemma equivalencesP r x: inc r (equivalences x) <-> (equivalence_on r x).
proof: Proof. split; first by move /Zo_hi. move => pa; apply:Zo_i => //; apply/setP_P. move: pa => [[xx _ _ _] <-]. by move: (sub_graph_coarse_substrate xx). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)