proposition: Lemma inl_map2_compat_prop0 S S' u x i j: inl_same_index S S' -> inl_map2_compat S S' u -> inc x (Vg (isE S) i) -> gle (isr S) i j -> Vf (Vg (isf S') (J i j)) (Vf (Vg u i) x) = Vf (Vg u j) (Vf (Vg (isf S) (J i j)) x).
proof: Proof. move => ha [hb1 hb2 hb3 hb4] xe lij. move: (inl_prop0 lij) => [iI jI]. have lij': gle (isr S') i j by rewrite - ha. move: (hb3 _ iI) => [fui sui tui]. move: (hb3 _ jI) => [fuj suj tuj]. move: (inl_prop4 lij) => [fij sij tij]. move: (inl_prop4 lij') => [fij' sij' tij']. have co1: Vg u j \coP Vg (isf S) (J i j) by split => //; ue. have co2: Vg (isf S') (J i j) \coP Vg u i by split => //; ue. have xs1: inc x (source (Vg u i)) by ue. have xs2: inc x (source (Vg (isf S) (J i j))) by ue. move: (f_equal (Vf ^~x) (hb4 _ _ lij)); rewrite ! compfV//. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)