proposition: Lemma noid_prop0 i: inc i I -> sub (Vg noid_E i) (Vg E i).
proof: Proof. move => iI. rewrite /noid_E; aw. have ii: inc (J i i) r by apply: (proj32 preorder_r i); rewrite substrate_r. case:(function_f ii); aw => ff sf <-; rewrite LgV//. apply: (Imf_Starget ff). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)