proposition: Lemma transport : SU.LU2SemiU (SUs, SUt0, SUt1) -> SysF_TYP (sval HM_W2).
proof: Proof. move=> [φ] [ψ0] [ψ1] [Hφψ0 HHφψ1]. apply: (SysF_TYPI (map tidy [])). apply /(svalP HM_W2) /(svalP HM_W1). have := iffRL (pure_typable_tidy_iff _ (Gamma1 := [])). move=> /(_ [many_poly_abs 2 t_0_W; many_poly_abs n_W t_1_W]). apply; first by apply: prenex_Gamma_W. apply: (pure_typable_M_W φ ψ0 ψ1). apply: typing_P_W. apply: typing_Q_W; [apply: typing_x_1_W | apply: typing_x_2_W]; by eassumption. 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