proposition: Lemma inl_dl_bijection: bijection_prop (inductive_map S inl_dl_fu (inductive_limit inl_dl_systemS')) (inductive_limit S) (inductive_limit inl_dl_systemS').
proof: Proof. have H := inl_dl_fu_compat. move:(proj1 (inl_map_prop H)). set mfun := inductive_map _ _ _; move => [ff sf tf]. have imf:injection mfun. apply /(inl_map_injective H) => p x y ps xE yE. move:(ps); rewrite inl_dl_I => /setX_P [pp iI lL]. move:(proj1 (inl_dl_fh_cp ps)) => ha. move:(inl_dl_fg_prop1 (P p) lL); set fa := inl_can_fun _ _ => eq1. have iI': inc (P p) (isI (inl_dl_S_lambda lL)) by []. case:(inl_can_fun_fp iI'); rewrite -/fa => ffa sfa tfa. have sfa':source fa = Vg (isE S) p. by move: sfa; rewrite /= /inl_dl_Elam_fam LgV// pp. have xs: inc x (source (inl_dl_fg (P p) (Q p))) by rewrite eq1 sfa'. have ys: inc y (source (inl_dl_fg (P p) (Q p))) by rewrite eq1 sfa'. have xs':inc x (Vg (isE (inl_dl_S_lambda lL)) (P p)) by rewrite - sfa sfa'. have ys':inc y (Vg (isE (inl_dl_S_lambda lL)) (P p)) by rewrite - sfa sfa'. rewrite /inl_dl_fu; rewrite LgV// ! compfV // eq1 /fa. have lL':inc (Q p) (isI inl_dl_systemS') by []. rewrite (inl_can_fun_ev iI' xs') (inl_can_fun_ev iI' ys'). have eq2: (Vg (isE inl_dl_systemS') (Q p)) = inductive_limit (inl_dl_S_lambda lL). by rewrite /= LgV //inl_dl_F_lambda_prop. have fxs: inc (class (inl_equiv (inl_dl_S_lambda lL)) (J x (P p))) (Vg (isE inl_dl_systemS') (Q p)). by rewrite eq2; apply: inl_class_in_lim. have fys: inc (class (inl_equiv (inl_dl_S_lambda lL)) (J y (P p))) (Vg (isE inl_dl_systemS') (Q p)). by rewrite eq2; apply: inl_class_in_lim. rewrite (inl_can_fun_ev lL' fxs) (inl_can_fun_ev lL' fys). move/(inl_class_eq_bis lL' lL' fxs fys) => [i]; aw. move => [ai _]; rewrite /= LgV//- inl_dl_hml_invariant. have cc:= (inl_dl_halm_compat ai). have cc':inl_same_index (inl_dl_S_lambda (pidl_i1_L sr2 ai)) (inl_dl_S_lambda (pidl_i2_L sr2 ai)) by []. rewrite (inl_map_val_aux2 cc' cc iI xs') (inl_map_val_aux2 cc' cc iI ys'). rewrite /inl_dl_halm_fam LgV //. move/(inl_class_eq_bis); simpl; rewrite pp /inl_dl_Elam_fam LgV// => Hx. have lea: gle (isr S) p (J (P p) i). rewrite - {1} pp Sr; apply/pidl_gleP1; split => //. by apply: (proj32 or1); rewrite sr1. move :(inl_prop4 lea) => [fb sb tb]. have xs2:inc (Vf (Vg (isf S) (J p (J (P p) i))) x) (Vg (isE S) (J (P p) i)). Wtac. have ys2:inc (Vf (Vg (isf S) (J p (J (P p) i))) y) (Vg (isE S) (J (P p) i)). Wtac. move: (Hx iI iI xs2 ys2) => [j []]; simpl; aw => leb _. have lec: gle (isr S) (J (P p) i) (J j i). rewrite Sr; apply/pidl_gleP1; split => //. apply: (proj32 or2); exact: (arg2_sr ai). rewrite /inl_dl_glam_fam LgV//; aw. rewrite inl_prop3 // inl_prop3 // => h. by exists (J j i) => //; rewrite - pp Sr; apply/pidl_gleP1. split => //; split => //. split => //; rewrite sf tf => y /inductive_limit_hi /= []. set l := (Q (rep y)) => lL. rewrite LgV // inl_dl_F_lambda_prop. move => /inductive_limit_hi /= []; set i:= (Q (rep (P (rep y)))) => iI. have ilI: inc (J i l) (isI S) by rewrite inl_dl_I; apply: setXp_i. move:(proj1 (inl_dl_fh_cp ilI)); aw => co1. set x:= P _; rewrite /inl_dl_Elam_fam LgV//; move => xE -> ->. exists (class (inl_equiv S) (J x (J i l))). apply: (inl_class_in_lim ilI xE). rewrite /mfun; rewrite (inl_inductive_map_ev inl_dl_fu_compat ilI xE). rewrite /inl_dl_fu (LgV ilI) pr1_pair pr2_pair. have iI':inc i (isI (inl_dl_S_lambda lL) ) by []. have xEb: (Vg (isE (inl_dl_S_lambda lL)) i) = Vg (isE S) (J i l). rewrite /= /inl_dl_Elam_fam LgV//. have xE': inc x (Vg (isE (inl_dl_S_lambda lL)) i) by rewrite xEb. move:(inl_can_fun_fp iI') => [fcf scf tcf]. have xE'':inc x (source (inl_can_fun (inl_dl_S_lambda lL) i)) by ue. move: co1; rewrite inl_dl_fg_prop1 => co1; rewrite compfV//. have ww: inc (Vf (inl_can_fun (inl_dl_S_lambda lL) i) x) (Vg (isE inl_dl_systemS') l). move: tcf;simpl;rewrite LgV // inl_dl_F_lambda_prop => <-; Wtac. have eq1:= (inl_can_fun_ev iI' xE'). by rewrite eq1 inl_can_fun_ev // - eq1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)