proposition: Lemma ex7_eqv_prop3 i j: gle (isr S) i j -> compatible_with_equivs (Vg (isf S) (J i j)) (ex7_eqv i)(ex7_eqv j).
proof: Proof. move => leij. move:(inl_prop0 leij) => [iI jI]. move:(ex7_eqv_prop1 iI) (ex7_eqv_prop1 jI) => [ha hb ][hc hd]. move: (inl_prop4 leij) => [fij sij tij]. have tij': target (Vg (isf S) (J i j)) = substrate (ex7_eqv j) by ue. have sij': source (Vg (isf S) (J i j)) = substrate (ex7_eqv i) by ue. apply:(compatible_with_pr2 ha hc fij tij' sij'). move => x y /(ex7_eqv_prop2 iI) [xE yE sc]. have pa: inc (Vf (Vg (isf S) (J i j)) x) (Vg (isE S) j) by Wtac. have pb: inc (Vf (Vg (isf S) (J i j)) y) (Vg (isE S) j) by Wtac. apply/(ex7_eqv_prop2 jI); split => //. by rewrite (inl_class_of_fij leij xE) (inl_class_of_fij leij yE). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)