proposition: Lemma pure_typing_trace_poly_typeE {s ns Gamma t n}: is_simple s -> allfv_poly_type (gt (length ns)) s -> pure_typing ((map (fun x => poly_var (n + x)) ns) ++ poly_abba :: Gamma) (trace_poly_type (length ns) s) t -> ren_poly_type (fun x => n + nth x ns 0) s = tidy t.
proof: Proof. elim: s Gamma t n. - move=> x Gamma t n _ /= ? /pure_typingE [n1] [?] [?]. rewrite ?nth_error_map nth_error_app1; first by rewrite map_length; lia. rewrite nth_error_map. have -> := nth_error_nth' ns 0; first by lia. move: (nth x ns 0) => y [[?]] []. subst. move=> /containsE ? ->. subst. rewrite tidy_many_poly_abs_le /=; first by lia. congr poly_var. by lia. - move=> s1 IH1 s2 IH2 Gamma t n /= [/IH1 {}IH1 /IH2 {}IH2] [/IH1 {}IH1 /IH2 {}IH2]. move=> /pure_typingE [n1] [?] [?] [?] [+] [+] [H1C ?]. subst. move=> /pure_typingE' [?] [?] [+] [+] H2C. move=> /pure_typingE' [?] [+] H3C. rewrite ?nth_error_map nth_error_app2; first by rewrite ?map_length; lia. rewrite ?map_length (ltac:(lia) : length ns - length ns = 0) /=. move=> [?]. subst. move: H3C => /(contains_poly_arrE (n := 2)) => - [[|r1 [|r2 [|? ?]]]] [] //=. move=> _ [? ?]. subst. move: H2C => /containsE [? ?]. subst. move: H1C => /containsE ?. subst. rewrite ?map_app /= ?map_map /=. under [map _ ns]map_ext => x do rewrite (ltac:(lia) : n1 + (n + x) = (n1 + n) + x). move=> /IH2 {}IH2 /IH1 {}IH1. rewrite -tidy_many_poly_abs_tidy /= -IH1 -IH2. rewrite tidy_many_poly_abs_le /=. { rewrite ?allfv_poly_type_ren_poly_type /=. constructor; apply: allfv_poly_type_TrueI; by lia. } rewrite IH1 IH2 ?tidy_tidy -IH1 -IH2 ?poly_type_norm /=. congr poly_arr; apply: extRen_poly_type; by lia. - done. Qed.
imports: List Lia Relation_Definitions Relation_Operators Operators_Properties Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util(Facts poly_type_facts pure_term_facts term_facts typing_facts iipc2_facts pure_typing_facts) ssreflect ssrbool ssrfun