proposition: Lemma ex7_fij_ev i j x: gle (isr S) i j -> inc x (ex7_Ei i) -> Vf (ex7_fij i j) x = class (ex7_eqv j) (Vf (Vg (isf S) (J i j)) (rep x)).
proof: Proof. move => lij xE; move:(inl_prop0 lij) => [iI jI]. move:(ex7_eqv_prop1 iI) (ex7_eqv_prop1 jI) => [ha hb ][hc hd]. move: (inl_prop4 lij) => [fij sij tij]. rewrite /ex7_fij foqcs_V //; ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)