proposition: Lemma ex6_F_prop2 y i j j': inc i (Vg Jf j) -> inc y (Vg (isE S) i) -> gle rL j j' -> ex6_F_val y i j = ex6_F_val y i j'.
proof: Proof. move => iJl yEi lejj. move:(arg1_sr lejj)(arg2_sr lejj); rewrite HLs => jL jL'. move:(ex6_prop5b jL) => [ra rb _ _]. move:(ex6_prop5b jL') => [ra' rb' _ _]. have iJl': inc i (Vg Jf j') by apply:(HJm lejj). have cyE: inc (class (inl_equiv (ex6_systemi j)) (J y i)) (Vg (isE ex6_F) j). simpl;rewrite LgV//; apply: inl_class_in_lim; rewrite ?ra ?rb //; rewrite LgV//. have cyE': inc (class (inl_equiv (ex6_systemi j')) (J y i)) (Vg (isE ex6_F) j'). simpl; rewrite LgV//; apply: inl_class_in_lim; rewrite ?ra' ?rb' //; rewrite LgV//. have yEj: inc y (Vg (isE (ex6_systemi j')) i). rewrite (proj41 (ex6_prop5b jL')); rewrite LgV//. have jj: gle rL j' j' by apply: (proj32 HLp); rewrite HLs. apply/inl_class_eq_bis => //; exists j'; aw; split => //=; rewrite !LgV//. rewrite ! ex6_gij_prop1 {1}(ex6_prop6b lejj) (ex6_prop6b jj). rewrite inl_restr_cf_ev // inl_restr_cf_ev //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)