proposition: Lemma ex7_eqv_prop2 i: inc i (isI S) -> forall x y, related (ex7_eqv i) x y <-> [/\ inc x (Vg (isE S) i), inc y (Vg (isE S) i) & class (inl_equiv S) (J x i) = class (inl_equiv S) (J y i)].
proof: Proof. move => iI x y. move:(inl_can_fun_fp iI) => [fi si ti]. split. case/(ea_relatedP fi); rewrite si => xE yE. by rewrite (inl_can_fun_ev iI xE) (inl_can_fun_ev iI yE). move => [xE yE etc]; apply/(ea_relatedP fi); rewrite si; split => //. by rewrite (inl_can_fun_ev iI xE) (inl_can_fun_ev iI yE). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)