proposition: Lemma inverse_transport : SysF_TC (Gamma_M0, M_M0, t_M0) -> SysF_TYP M0.
proof: Proof. move=> /pure_typing_iff_type_assignment. rewrite /Gamma_M0 /M_M0 /t_M0. move=> /pure_typingE' [?] [?] [_] [/pure_typableI HM0 _]. have : exists Gamma, pure_typable Gamma M0. { elim: (pure_var_bound M0) ([poly_abs (poly_var 0)]) HM0. - move=> /= ? ?. eexists. by eassumption. - by move=> {}n IH Gamma /= /pure_typableE [?] /IH. } move=> [Gamma] [t] /pure_typing_to_typing [P] [->]. move=> /typing_to_type_assignment ?. by exists Gamma, t. Qed.
imports: List Lia Relation_Operators Undecidability.SystemF.SysF Undecidability.SystemF.Util(Facts poly_type_facts pure_term_facts term_facts typing_facts pure_typing_facts) ssreflect ssrbool ssrfun