proposition: Lemma inl_map_compat0 S u F i j x: inl_map_compat S u F -> gle (isr S) i j -> inc x (Vg (isE S) i) -> (Vf (Vg u i)) x = Vf (Vg u j) (Vf (Vg (isf S) (J i j)) x).
proof: Proof. move => [a hb hc hd] lij xi. move:(inl_prop0 lij) => [iI jI]. move: (inl_prop4 lij) => [fij sij tij]. move:(hc _ jI) => [fu su tu]. have co: Vg u j \coP Vg (isf S) (J i j) by split => //; ue. have xs: inc x (source (Vg (isf S) (J i j))) by ue. rewrite -(hd _ _ lij); rewrite compfV//. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)