proposition: Lemma inl_dl2_res2: inl_map2_compat inl_dl2_limlim inl_dl2_limlim' inl_dl2_v_fam.
proof: Proof. rewrite /inl_dl2_v_fam; split. - fprops. - by aw. - move => i /= iI2; rewrite !LgV//. move:(inl_dl2_res1 iI2) => [ha hb]. exact: (proj1 (inl_map2_prop ha hb)). - move => i j /= leij'. move:(arg1_sr leij')(arg2_sr leij'); rewrite sr2 => iI2 jI2. rewrite !LgV ///inl_dl_hlm_gen; case: (ixm (inc (J i j) r2)) => // leij. clear leij'. set V := inl_dl2_v. set hlm := inl_dl_hlm or1 or2 sr1 sr2 dr1 Sr (pidl_i3_L or2 leij). set hlm' := inl_dl_hlm or1 or2 sr1 sr2 dr1 Sr' (pidl_i3_L or2 leij). move:(inl_dl2_res1 iI2)(inl_dl2_res1 jI2) =>[ha hb][ha' hb']. move: (inl_map2_prop3 ha hb) (inl_map2_prop3 ha' hb'). rewrite -/(inl_dl2_v _) -/(inl_dl2_v _) -/V. set Si := inductive_limit _; set Si' := inductive_limit _. set Sj := inductive_limit _; set Sj' := inductive_limit _. move => [[fvi svi tvi] Vip] [[fvj svj tvj] Vjp]. set T := inl_dl_S_lambda or1 or2 sr1 sr2 dr1 Sr. set T' := inl_dl_S_lambda or1 or2 sr1 sr2 dr1 Sr'. have sid1:inl_same_index (T _ (pidl_i1_L sr2 leij)) (T _ (pidl_i2_L sr2 leij)) by []. set QQ := inl_dl_halm_compat or1 or2 sr1 sr2 dr1. move: (inl_map2_prop3 sid1 (QQ _ Sr _ _ leij)). simpl; rewrite -/(inl_dl_hlm _ _ _ _ _ _ _) inl_dl_hml_invariant. have ->: (inl_dl_hlm_gen or1 or2 sr1 sr2 dr1 Sr (J i j)) = hlm. by rewrite /hlm inl_dl_hml_invariant; aw. rewrite -inl_dl_F_lambda_prop -inl_dl_F_lambda_prop. rewrite /inl_dl_F_lambda -/Si - /Sj. move => [[fLa sLa tLa] Lap]. have sid2:inl_same_index (T' _ (pidl_i1_L sr2 leij)) (T' _ (pidl_i2_L sr2 leij)) by []. move:(inl_map2_prop3 sid2 (QQ _ Sr' _ _ leij)). simpl; rewrite -/(inl_dl_hlm _ _ _ _ _ _ _) inl_dl_hml_invariant. have ->: (inl_dl_hlm_gen or1 or2 sr1 sr2 dr1 Sr' (J i j)) = hlm'. by rewrite /hlm' inl_dl_hml_invariant; aw. rewrite- inl_dl_F_lambda_prop -inl_dl_F_lambda_prop. rewrite /inl_dl_F_lambda -/Si' - /Sj'. move => [[fLb sLb tLb] Lbp]. have res1: V j \coP hlm by split => //; ue. have res2: hlm' \coP V i by split => //; ue. apply:function_exten. + by apply: compf_f. + by apply: compf_f. + aw; ue. + aw; ue. + aw; rewrite svi => x xsi. have xs1:inc x (source (V i)) by ue. have xs2: inc x (source hlm) by ue. rewrite ! compfV //. have qe: isI (inl_dl2_Slambda i) = I1. rewrite /inl_dl2_Slambda /inl_dl_system_S_lambda. by case: (ixm (inc i I2)). have qe': isI (inl_dl2_Slambda j) = I1. rewrite /inl_dl2_Slambda /inl_dl_system_S_lambda. by case: (ixm (inc j I2)). move/inductive_limit_hi: xsi;set k := Q _ ; set xk := P _. move=> [ra rb ->]; rewrite (Vip _ _ ra rb). move:(ra). rewrite qe - qe' => ra'. move: ra; rewrite qe => kI1. have rb1: inc xk (Vg (isE S) (J k i)). move: rb; rewrite /inl_dl2_Slambda /inl_dl_system_S_lambda. case: (ixm (inc i I2)) => // HH. by rewrite /= /inl_dl_Elam_fam LgV. have rb2: inc xk (Vg (inl_dl_Elam_fam I1 S i) k). by rewrite /inl_dl_Elam_fam LgV. have kiI: inc (J k i) (isI S). rewrite - is_substrate_r Sr (proj2(pidl_or or1 or2 sr1 sr2)); fprops. move: (proj43 compat_u _ kiI) => [fuki suki tuki]. set xk1 := (Vf (Vg u (J k i)) xk). have ukixE: inc xk1 (Vg (inl_dl_Elam_fam I1 S' i) k). rewrite /xk1 /inl_dl_Elam_fam LgV//; Wtac. rewrite /inl_dl2_ulam_fam LgV//. move: (Lbp k xk1 kI1 ukixE). set c1 := class _ (J xk1 k). set c2 := class _ (J xk1 k). have cc : c1 = c2. rewrite /c1 /c2 /T' /inl_dl2_Slambda' /inl_dl_system_S_lambda. by case: (ixm (inc i I2)). rewrite cc => ->; clear c1 c2 cc. move: (Lap k xk kI1 rb2). set c1 := class _ (J xk k). set c2 := class _ (J xk k). have cc : c1 = c2. rewrite /c1 /c2 /T /inl_dl2_Slambda /inl_dl_system_S_lambda. by case: (ixm (inc i I2)). rewrite cc => ->; clear c1 c2 cc. set xk2:= (Vf (Vg (inl_dl_halm_fam I1 S i j) k) xk). have gle0: gle (isr S) (J k i) (J k j). rewrite Sr; apply/pidl_gleP1; split => //. by apply: (proj32 or1); rewrite sr1. move/inl_prop4: (gle0) =>[ff sf tf]. have rb3: inc xk2 (Vg (isE (inl_dl2_Slambda j)) k). rewrite /inl_dl2_Slambda /inl_dl_system_S_lambda. case: (ixm (inc j I2)) => // H. rewrite /= /inl_dl_Elam_fam /xk2 /inl_dl_halm_fam ! LgV//; Wtac. rewrite /inl_dl_halm_fam LgV//. move: (Vjp k xk2 ra' rb3). set c1 := class _ (J xk2 k). set c2 := class _ (J xk2 k). have cc : c1 = c2. rewrite /c1 /c2 /T /inl_dl2_Slambda /inl_dl_system_S_lambda. by case: (ixm (inc j I2)). rewrite cc; move ->; clear c1 c2 cc. rewrite /inl_dl2_ulam_fam LgV //. congr class; last (congr J). rewrite /T'/inl_dl2_Slambda'/ inl_dl_system_S_lambda. by case: (ixm (inc j I2)). have kjI: inc (J k j) (isI S). rewrite - is_substrate_r Sr (proj2(pidl_or or1 or2 sr1 sr2)); fprops. move: (proj43 compat_u _ kjI) => [fukj sukj tukj]. move: (gle0); rewrite Sr - Sr' => /inl_prop4[ff' sf' tf']. have co1: Vg u (J k j) \coP Vg (isf S) (J (J k i) (J k j)) by split => //; ue. have co2: Vg (isf S') (J (J k i) (J k j)) \coP Vg u (J k i) by split => //; ue. have xkE': inc xk (source (Vg (isf S) (J (J k i) (J k j)))) by ue. have xkE: inc xk (source (Vg u (J k i))) by ue. move:(f_equal (Vf ^~xk) (proj44 compat_u _ _ gle0)). rewrite !compfV //; move ->; rewrite /xk2 /inl_dl_halm_fam ! LgV//. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)