proposition: Lemma inl_subfam_prop3 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)) (u := (inductive_limit_fun S' S (Lg (isI S) ji))): forall i x, inc i (isI S) -> inc x (Vg M i) -> Vf u (class (inl_equiv S') (J x i)) = class (inl_equiv S) (J x i).
proof: Proof. move => i x iI xE. have ha:inl_same_index S' S by []. have hb:= inl_subfam_compat H. move:(inl_map_val_aux2 ha hb iI xE); rewrite LgV// -/u ci_V //. by move: (H) => [_ _ hc _]; apply: hc. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)