proposition: Lemma inl_can_fun_inj S: (forall p, inc p (isr S) -> injection (Vg (isf S) p)) -> (forall i, inc i (isI S) -> injection (inl_can_fun S i)).
proof: Proof. move => h i iI. move:(inl_can_fun_fp iI) => [ff sf tf]. split => //; rewrite sf => x y xs ys. rewrite (inl_can_fun_ev iI xs) (inl_can_fun_ev iI ys). move/(inl_class_eq_bis iI iI xs ys) => [k []];aw; move => lij _ etc. move: (proj2 (h _ lij)); rewrite (proj32 (inl_prop4 lij)) => h'. exact:(h' _ _ xs ys etc). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)