proposition: Lemma inl_dl_fu_compat: inl_map_compat S inl_dl_fu (inductive_limit (inl_dl_systemS')).
proof: Proof. rewrite /inl_dl_fu; split; aww. move => i iI; rewrite LgV//; apply: (proj2 (inl_dl_fh_cp iI)). move => p1 p2 lep1p2. move:(inl_prop0 lep1p2) => [p1ii p2ii]; rewrite !LgV//. move: (lep1p2); rewrite Sr; move/pidl_gleP => [_ _ lea leb]. move: (p1ii) (p2ii); rewrite inl_dl_I. move => /setX_P [pp1 aI lL] /setX_P [pp2 bI mL]. have Fgbmv:= (inl_dl_fg_prop1 (P p2) mL). set Fhm := inl_can_fun inl_dl_systemS' (Q p2). set Fgbm := inl_dl_fg (P p2) (Q p2). set Ffbaml := Vg (isf S) (J p1 p2). set Fhl := inl_can_fun inl_dl_systemS' (Q p1). set Fgal := inl_dl_fg (P p1) (Q p1). have mI': inc (Q p2) (isI inl_dl_systemS') by []. move: (inl_can_fun_fp mI'); rewrite -/Fhm; move => [fhm shm thm]. move: (inl_dl_fg_fp bI mL); rewrite -/Fgbm; move => [fgbm sgbm tgbm]. move: (inl_dl_fg_fp aI lL); rewrite -/Fgal; move => [fgal sgal tgal]. move: (is_function_f lep1p2). rewrite -/Ffbaml; aw; move => [ffbaml sfbaml tfbaml]. have co1: Fhm \coP Fgbm. by split => //; rewrite shm tgbm /= (LgV mL) (inl_dl_F_lambda_prop mL). have co2:Fgbm \coP Ffbaml by split => //; rewrite sgbm pp2 tfbaml. rewrite -(compfA co1 co2). have lec: gle (isr S) (J (P p1) (Q p2)) p2. rewrite -{2} pp2 Sr; apply/pidl_gleP1; split => //. by apply: (proj32 or2); rewrite sr2. have led: gle (isr S) p1 (J (P p1) (Q p2)). rewrite -{1} pp1 Sr; apply/pidl_gleP1; split => //. by apply: (proj32 or1); rewrite sr1. move:(is_compose_f led lec); rewrite -/Ffbaml. set Ffbamm := Vg (isf S) (J (J (P p1) (Q p2)) p2). set Ffaalm := Vg (isf S) (J p1 (J (P p1) (Q p2))). move: (is_function_f lec) (is_function_f led);aw. rewrite -/Ffbamm -/Ffaalm; move => [ffbamm sfbamm tfbamm][ffaalm sfaalm tfaalm]. have co3: Fgbm \coP Ffbamm by split => //; rewrite sgbm tfbamm pp2. have co4: Ffbamm \coP Ffaalm by split => //; ue. move <-; rewrite (compfA co3 co4). have lee: gle (isr (inl_dl_S_lambda mL)) (P p1) (P p2) by []. move: (proj2 (inl_can_fun_prop lee)). rewrite - Fgbmv /= /inl_dl_glam_fam LgV//; aw; rewrite pp2 -/Ffbamm => <-. have eqx: Ffaalm = Vg (inl_dl_halm_fam (Q p1) (Q p2)) (P p1). by rewrite /inl_dl_halm_fam LgV//; rewrite pp1. set S1 := (inl_dl_S_lambda (pidl_i1_L sr2 leb)). set S2 := (inl_dl_S_lambda (pidl_i2_L sr2 leb)). have aI': inc (P p1) (isI S1) by []. have ssi: inl_same_index S1 S2 by []. move:(inl_map2_prop ssi (inl_dl_halm_compat leb)). set Fgam := inductive_limit_fun _ _ _. move=> [[fgam sgam tgam] vgam]. move:(vgam _ aI'); rewrite {1} /inl_dl_halm_fam LgV// pp1; move ->. rewrite - inl_dl_fg_prop1 -/Fgal. have co5: Fhm \coP Fgam. by split => //; rewrite shm tgam /= LgV//; apply: inl_dl_F_lambda_prop. have co6: Fgam \coP Fgal by split => //; ue. rewrite (compfA co5 co6); congr compose. have : gle (isr inl_dl_systemS') (Q p1) (Q p2) by []. by move/inl_can_fun_prop => /proj2 /=; rewrite LgV// - inl_dl_hml_invariant. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)