proposition: Lemma inl_inductive_limit_fun_IV2 S1 S2 x S1' S2' x': inl_same_data S1 S1' -> inl_same_data S2 S2' -> x = x' -> inductive_limit_fun S1 S2 x = inductive_limit_fun S1' S2' x'.
proof: Proof. move => ha hb hc. rewrite /inductive_limit_fun -hc -(inductive_limit_Iv hb). have si2: (isI S2) = (isI S2') by rewrite -!is_substrate_r; case: hb => _ -> _. have <-: (inl_map2_aux S2 x) = (inl_map2_aux S2' x). rewrite /inl_map2_aux - si2; apply: Lg_exten => i ii. by rewrite (inl_can_fun_Iv i hb). by rewrite /inductive_map -(inductive_limit_Iv ha) /inl_map_val. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)