proposition: Lemma inl_subfam_prop4 S M (H:inl_subfam_hyp S M) (S' := (inductive_system_subsets H)) (ji := fun i => canonical_injection (Vg M i) (Vg (isE S) i)): injection_prop (inductive_limit_fun S' S (Lg (isI S) ji)) (inductive_limit S') (inductive_limit S).
proof: Proof. have II: isI S' = isI S by []. move: (inl_subfam_compat H) => cc. move: (H) => [ha hb hc hd]. rewrite/inductive_limit_fun /inductive_map; saw. apply:inl_limit_fun_inj => // i; rewrite II => iI; rewrite LgV//; apply:ci_fi; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)