proposition: Lemma ex7_eqv_prop1 i: inc i (isI S) -> equivalence_on (ex7_eqv i) (Vg (isE S) i).
proof: Proof. move => iI. move:(inl_can_fun_fp iI) => [fi si ti]. by move:(graph_ea_equivalence fi); rewrite si. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)