proposition: Lemma inl_dl2_res3 (bij1 := (inductive_map S (inl_dl_fu or1 or2 sr1 sr2 dr1 dr2 Sr) (inductive_limit (inl_dl_systemS' or1 or2 sr1 sr2 dr1 dr2 Sr)))) (bij2 := (inductive_map S' (inl_dl_fu or1 or2 sr1 sr2 dr1 dr2 Sr') (inductive_limit (inl_dl_systemS' or1 or2 sr1 sr2 dr1 dr2 Sr')))) (pl1 := inductive_limit_fun S S' u) (pl2 := inductive_limit_fun inl_dl2_limlim inl_dl2_limlim' inl_dl2_v_fam): [/\ bijection bij1, bijection bij2 & pl2 \co bij1 = bij2 \co pl1].
proof: Proof. move:(inl_map2_prop3 inl_dl2_SrSr compat_u) => /=. rewrite -/pl1. set E := (inductive_limit S); set E':= (inductive_limit S'). move => [[fpl1 spl1 tpl1] pl1_prop]. have ha: inl_same_index inl_dl2_limlim inl_dl2_limlim' by []. move: (inl_map2_prop3 ha inl_dl2_res2); simpl. rewrite -/pl2. set vE:= inductive_limit _; set vE':= inductive_limit _. move => [[fpl2 spl2 tpl2] pl2_prop]. move:(inl_dl_bijection or1 or2 sr1 sr2 dr1 dr2 Sr). move:(inl_dl_bijection or1 or2 sr1 sr2 dr1 dr2 Sr'). rewrite -/bij1 -/bij2 -/E -/E' -/vE -/vE'. move => [bp2 sf2 tf2] [bp1 sf1 tf1]. split => //. move:(bp2)(bp1) => [[ff1 _] _] [[ff2 _] _]. have co1: pl2 \coP bij1 by split => //; ue. have co2: bij2 \coP pl1 by split => //; ue. apply: function_exten;try (apply: compf_f => //); aw; try ue. rewrite sf1 => x /inductive_limit_hi. set il := Q _; set xb:= P _; move => [ilI hb ->]. have xs1: inc (class (inl_equiv S) (J xb il)) (source pl1). by rewrite spl1; apply: inl_class_in_lim. move: (xs1); rewrite spl1 - sf1 => xs2; rewrite !compfV //. have ilI':inc il (isI S') by rewrite -(inl_same_index_same_I inl_dl2_SrSr). rewrite (pl1_prop _ _ ilI hb). move: (proj43 compat_u _ ilI) =>[fu su tu]. have xs4:inc (Vf (Vg u il) xb) (Vg (isE S') il) by Wtac. move: (inl_dl_fu_compat or1 or2 sr1 sr2 dr1 dr2 Sr') => comp2. move: (inl_dl_fu_compat or1 or2 sr1 sr2 dr1 dr2 Sr) => comp1. rewrite /bij2 (inl_inductive_map_ev comp2 ilI' xs4). rewrite /bij1 (inl_inductive_map_ev comp1 ilI hb). move:(proj1 (inl_dl_fh_cp or1 or2 sr1 sr2 dr1 dr2 Sr ilI)) => cop1. move:(proj1 (inl_dl_fh_cp or1 or2 sr1 sr2 dr1 dr2 Sr' ilI')) => cop2. move:(ilI); rewrite - is_substrate_r Sr (proj2(pidl_or or1 or2 sr1 sr2)). move => /setX_P [pil iI1 lI2]. have xs3: inc xb (source (inl_dl_fg or1 or2 sr1 sr2 dr1 Sr (P il) (Q il))). move:(inl_dl_fg_fp or1 or2 sr1 sr2 dr1 Sr iI1 lI2)=> [ff sf tf]. by rewrite sf pil. have xs5: inc (Vf (Vg u il) xb) (source (inl_dl_fg or1 or2 sr1 sr2 dr1 Sr' (P il) (Q il))). move:(inl_dl_fg_fp or1 or2 sr1 sr2 dr1 Sr' iI1 lI2)=> [ff sf tf]. rewrite sf pil; Wtac. rewrite /inl_dl_fu ! LgV// !compfV //. rewrite inl_dl_fg_prop1 inl_dl_fg_prop1. have ra: inc (P il)(isI (inl_dl_S_lambda or1 or2 sr1 sr2 dr1 Sr lI2)) by []. have rb: inc xb (Vg (isE (inl_dl_S_lambda or1 or2 sr1 sr2 dr1 Sr lI2)) (P il)). by rewrite /= /inl_dl_Elam_fam LgV// pil. have ra':inc (Q il) (isI (inl_dl_systemS' or1 or2 sr1 sr2 dr1 dr2 Sr)) by []. have rb': inc (class (inl_equiv (inl_dl_S_lambda or1 or2 sr1 sr2 dr1 Sr lI2)) (J xb (P il))) (Vg (isE (inl_dl_systemS' or1 or2 sr1 sr2 dr1 dr2 Sr)) (Q il)). rewrite /= LgV//inl_dl_F_lambda_prop. by apply:inl_class_in_lim. rewrite (inl_can_fun_ev ra rb) (inl_can_fun_ev ra' rb'). have ra2: inc (P il)(isI (inl_dl_S_lambda or1 or2 sr1 sr2 dr1 Sr' lI2)) by []. have ra2':inc (Q il) (isI (inl_dl_systemS' or1 or2 sr1 sr2 dr1 dr2 Sr')) by []. have rb2: inc (Vf (Vg u il) xb) (Vg (isE (inl_dl_S_lambda or1 or2 sr1 sr2 dr1 Sr' lI2)) (P il)). by rewrite /= /inl_dl_Elam_fam LgV// pil. have rb2': inc (class (inl_equiv (inl_dl_S_lambda or1 or2 sr1 sr2 dr1 Sr' lI2)) (J (Vf (Vg u il) xb) (P il))) (Vg (isE (inl_dl_systemS' or1 or2 sr1 sr2 dr1 dr2 Sr')) (Q il)). rewrite /= LgV//inl_dl_F_lambda_prop. by apply:inl_class_in_lim. rewrite (inl_can_fun_ev ra2 rb2) (inl_can_fun_ev ra2' rb2'). rewrite (pl2_prop _ _ lI2 rb')/ inl_dl2_v_fam LgV//. move:(inl_dl2_res1 lI2) => [rxa rxb]. move: (inl_map2_prop3 rxa rxb) => [bof hh]. have ra3: inc (P il) (isI (inl_dl2_Slambda (Q il))). rewrite /inl_dl2_Slambda /inl_dl_system_S_lambda. by case: (ixm (inc (Q il) I2)). have rb3: inc xb (Vg (isE (inl_dl2_Slambda (Q il))) (P il)). rewrite /inl_dl2_Slambda /inl_dl_system_S_lambda. by case: (ixm (inc (Q il) I2)). move:(hh (P il) xb ra3 rb3); rewrite -/(inl_dl2_v (Q il)). rewrite /inl_dl2_Slambda /inl_dl2_Slambda' /inl_dl_system_S_lambda. case: (ixm (inc (Q il) I2)) => // Ha ->. by rewrite/inl_dl2_ulam_fam LgV// pil. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)