proposition: Lemma inl_subfam_compat 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)): inl_map2_compat S' S (Lg (isI S) ji).
proof: Proof. move: (H) => [ha hb hc hd]. have II: isI S' = isI S by []. have rr: (isr S') = (isr S) by []. have he: inl_same_index S S' by []. split; aww. by rewrite /ji;move => i ii; rewrite LgV//; apply:ci_fp; apply: hc; rewrite - II. move => i j lij. case:(inl_prop0 lij); rewrite II => iI jI; rewrite LgV// LgV//. move: (hc _ iI) (hc _ jI) => s1 s2. move:(ci_fp s1); rewrite-/(ji i); move => [fci sci tci]. move:(ci_fp s2); rewrite-/(ji j); move => [fcj scj tcj]. move:(inl_prop4 lij) => [fij' sij' tij']. rewrite rr in lij. move:(inl_prop4 lij) => [fij sij tij]. have co1: Vg (isf S) (J i j) \coP ji i by split => //; ue. have co2: ji j \coP Vg (isf S') (J i j) by split => //; ue. apply:function_exten. + by apply:compf_f. + by apply:compf_f. + aw; ue. + aw; ue. + aw; rewrite sci => x xM. have qa: inc x (source (ji i)) by ue. have qb: inc x (source (Vg (isf S') (J i j))) by ue. have qc: (Vf (Vg (isf S') (J i j)) x) = Vf (Vg (isf S) (J i j)) x. rewrite /=/inl_subfam_fct LgV//; aw; rewrite restriction2_V //. by split => //; try ue; apply: hd. rewrite !compfV// qc/ji !ci_V//; apply: (hd _ _ lij). have hf:sub (Vg M i) (source (Vg (isf S) (J i j))) by ue. apply/(Vf_image_P fij hf); ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)