proposition: Lemma noid_prop5d i: inc i r -> function_prop (Vg noid_g i) (Vg noid_E' (P i)) (Vg noid_E' (Q i)).
proof: Proof. move => ir; rewrite /noid_g LgV//. exact: (restriction2_prop (noid_prop5b ir)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)