proposition: Lemma ex7_fij_ev_bis i j x: gle (isr S) i j -> inc x (Vg (isE S) i) -> Vf (ex7_fij i j) (class (ex7_eqv i) x) = class (ex7_eqv j) (Vf (Vg (isf S) (J i j)) 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]. have cq:inc (class (ex7_eqv i) x) (ex7_Ei i) by apply: inc_class_setQ; ue. have xe': inc x (substrate (ex7_eqv i)) by ue. move: (related_rep_class ha xe')=> /(ex7_eqv_prop2 iI) [ra rb rc]. move: (inl_prop4 lij) => [fij sij tij]; rewrite (ex7_fij_ev lij cq). suff: (related (ex7_eqv j) (Vf (Vg (isf S) (J i j)) (rep (class (ex7_eqv i) x))) (Vf (Vg (isf S) (J i j)) x)). by case/(related_equiv_P hc). apply/(ex7_eqv_prop2 jI); split => //; try Wtac. rewrite inl_class_of_fij // - rc inl_class_of_fij //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)