proposition: Lemma GE_I_Ev E x: inc x E -> Vg (GE_I E) x = x.
proof: Proof. move => xE. have : inc (J x x) (GE_I E) by apply/GE_I_incP; saw; fprops. by move/(pr2_V (GE_I_fgraph E)); aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)