fact: Definition inl_map_compat S u F:= [/\ fgraph u, domain u = isI S, forall i, inc i (isI S) -> function_prop (Vg u i) (Vg (isE S) i) F & forall i j, gle (isr S) i j -> (Vg u j) \co Vg (isf S) (J i j) = Vg u i].
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)