proposition: Lemma noid_prop5e i: inc i I -> Vg noid_g (J i i) = identity (Vg noid_E' i).
proof: Proof. move => iI. have ii: inc (J i i) r by apply: (proj32 preorder_r i); rewrite substrate_r. move:(compose_f ii ii) => cc. move:(function_f ii); aw; move => [ff sf tf]. move:(noid_prop5d ii); aw => fp; apply: (identity_prop0 fp) => x xM. rewrite (noid_prop5c ii xM). move:xM; rewrite /noid_E' LgV//; move/(Imf_P ff); rewrite sf. move => [u uE ->]; rewrite - {3}cc compfV //; [ split => //; ue | ue ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)