proposition: Lemma inl_map_val_aux2 S S' u i x (f := inductive_limit_fun S S' u) : inl_same_index S S' -> inl_map2_compat S S' u -> inc i (isI S) -> inc x (Vg (isE S) i) -> Vf f (class (inl_equiv S) (J x i)) = class (inl_equiv S') (J (Vf (Vg u i) x) i).
proof: Proof. move => hb ha iI xE. move:(ha) => [hu1 hu2 hu3 hu4]. move:(inl_map2_prop1 hb ha) => hc. have II:= (inl_same_index_same_I hb). have iI': inc i (isI S') by ue. move: (hu3 _ iI) => [fu su tu]. have uiE: inc (Vf (Vg u i) x) (Vg (isE S') i) by Wtac. have xE': inc x (source (Vg u i)) by ue. have cop:inl_can_fun S' i \coP Vg u i. by move:(inl_can_fun_fp iI') => [fc sc tc]; split => //; ue. rewrite /f/inductive_limit_fun (inl_inductive_map_ev hc iI xE)/inl_map2_aux. by rewrite LgV// compfV// inl_can_fun_ev. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)