proposition: Lemma inl_rem2_prop1: inl_map2_compat S inl_rem2_S' u.
proof: Proof. move: mcu => [ha hb hc hd]. split => //; first by move => i iI; simpl; rewrite LgV//; apply: hc. move => i j lij; move:(hd _ _ lij) => /= ->; rewrite LgV//. by move/hc:(proj1 (inl_prop0 lij)) => [fui _ <-]; apply: compf_id_l. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)