proposition: Lemma inl_sub_fam_im3: inl_subfam_hyp S inl_p7c2_Ni.
proof: Proof. move: a_fam_prop => [ha hb hc hd]. set Mi := Lg (isI S) (fun i => (singleton (Vg a_fam i))). have ->: inl_p7c2_Ni = Lg (isI S) (fun i => Vfi (Vg u i) (Vg Mi i)). apply: Lg_exten => i iS; rewrite /Mi LgV//. have II:= (inl_same_index_same_I sii). rewrite/Mi; apply: inl_sub_fam_im2; split; aww. move => i iI t; rewrite LgV; [ by move/set1_P ->; apply: hc | ue]. move => p pr. move:(proj31 (is_preorder_r S') _ pr) => pp. move:(pr); rewrite -{1} pp => /inl_prop0; rewrite - II; move => [iI jI]. move: (is_function_f pr) => [fi si ti]. have xa: inc (Vg a_fam (P p)) (source (Vg (isf S') p)). by rewrite si; apply: hc; rewrite - II. by rewrite ! LgV// (fun_image_set1 fi xa) (hd _ pr). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)