proposition: Lemma inverse_transport : SysF_TYP (sval HM_W2) -> SU.LU2SemiU (SUs, SUt0, SUt1).
proof: Proof. move=> [Gamma] [t] /pure_typing_iff_type_assignment. move=> /pure_typing_tidyI /pure_typableI /(svalP HM_W2) /(svalP HM_W1). move=> [?] /(pure_typing_ren_pure_term_allfv_pure_term id (Delta := map tidy Gamma_W)). apply: unnest; first done. rewrite ren_pure_term_id => /pure_typableI. move=> /(pure_typable_tidy_iff (Gamma1 := [])). apply: unnest; first by apply: prenex_Gamma_W. move=> /decompose_M_W [?] /decompose_N_W [?] [σ] [->]. move=> [/decompose_x_W [?] + /decompose_x_W [?] +]. move=> /introduce_simple_substitutions [ψ0 ?] /introduce_simple_substitutions [ψ1 ?]. by exists (funcomp prune σ), ψ0, ψ1. Qed.
imports: List Lia Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Util(Facts poly_type_facts pure_term_facts term_facts typing_facts pure_typing_facts pure_typable_prenex) ssreflect ssrbool ssrfun