proposition: Lemma ex7_fij_prop4 i j : gle (isr S) i j -> injection (ex7_fij i j).
proof: Proof. move => lij. move: (inl_prop0 lij) => [iI jI]. move:(ex7_eqv_prop1 iI) (ex7_eqv_prop1 jI)=> [eqRi sRi][eqRj sRj]. move: (inl_prop4 lij) => [fij sij tij]. move: (ex7_fij_prop1 lij) => [fij' sij' tij']; split => //; rewrite sij'. move => x y xE yE; rewrite /= (ex7_fij_ev lij xE) (ex7_fij_ev lij yE) => eq1. move:(rep_i_sr eqRi xE); rewrite sRi => rxE. move:(rep_i_sr eqRi yE); rewrite sRi => ryE. have ha: inc (Vf (Vg (isf S) (J i j)) (rep x)) (substrate (ex7_eqv j)). rewrite sRj; Wtac. have hb: inc (Vf (Vg (isf S) (J i j)) (rep y)) (substrate (ex7_eqv j)). rewrite sRj; Wtac. move /(related_equiv_P eqRj): (And3 ha hb eq1) => /(ex7_eqv_prop2 jI). move => [_ _]; rewrite inl_class_of_fij // inl_class_of_fij // => cc. rewrite -(class_rep eqRi xE) -(class_rep eqRi yE). apply:(class_eq1 eqRi). by apply/(ex7_eqv_prop2 iI). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)