proposition: Lemma typing_tidyI {Gamma P t} : typing Gamma P t -> exists Q, erase P = erase Q /\ typing (map tidy Gamma) Q (tidy t).
proof: Proof. elim: P Gamma t. - move=> x Gamma t /typingE Hx. exists (var x). constructor; first done. apply: typing_var. by rewrite nth_error_map Hx. - move=> P IHP Q IHQ Gamma t /typingE [?] /= [/IHP [P'] [->] {}IHP /IHQ [Q'] [->] {}IHQ]. exists (app P' Q'). constructor; first done. apply: typing_app; by eassumption. - move=> s P IH Gamma t /typingE [?] /= [->] /IH [P'] [->] HP'. exists (abs (tidy s) P'). constructor; first done. by apply: typing_abs. - move=> P IH s Gamma t /typingE [t'] /= [->] /IH [P'] [->]. move=> /typing_contains. apply. by apply /contains_tidyI /rt_step /contains_step_subst. - move=> P IH Gamma t /typingE [t'] /= [->] /IH [P'] [->] /=. case Hb: (fresh_inb _ _). + move=> /(typing_ren_poly_type (0 .: id)) => H. exists (ren_term (0 .: id) id P'). constructor; first by rewrite erase_ren_term_id. congr typing: H. rewrite ?map_map. apply: map_ext => ?. by rewrite tidy_ren_poly_type ?poly_type_norm /= ren_poly_type_id. + move=> H. exists (ty_abs P'). constructor; first done. apply: typing_ty_abs. congr typing: H. rewrite ?map_map. apply: map_ext => ?. by apply: tidy_ren_poly_type. 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) ssreflect ssrbool ssrfun