proposition: Lemma noid_prop5c i j x: gle r i j -> inc x (Vg noid_E' i) -> Vf (Vg noid_g (J i j)) x = Vf (Vg f (J i j)) x.
proof: Proof. move => lij xm. have hb':inc x (Vg noid_E' (P (J i j))) by aw. rewrite /noid_g -(restriction2_V (noid_prop5b lij) hb') LgV//. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)