proposition: Lemma inl_map2_prop3 S S' u (f := inductive_limit_fun S S' u): inl_same_index S S' -> inl_map2_compat S S' u -> function_prop f (inductive_limit S) (inductive_limit S') /\ forall i x, 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 => Ha Hu; split. exact: (proj1 (inl_map2_prop Ha Hu)). move=> i x ii xx; exact: (inl_map_val_aux2 Ha Hu ii xx). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)