proposition: Lemma inl_map2_prop2 S u i t: inc i (isI S) -> inc t (source (Vg u i)) -> function (Vg u i) -> target (Vg u i) = Vg (isE S) i -> Vf (Vg (inl_map2_aux S u) i) t = class (inl_equiv S) (J (Vf (Vg u i) t) i).
proof: Proof. move => iI tlim fu su. move: (inl_can_fun_fp iI) => [fc sc tc]. have hh:(inl_can_fun S i \coP Vg u i) by split => //; ue. rewrite /inl_map2_aux LgV// compfV// inl_can_fun_ev //; Wtac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)