proposition: Theorem reduction : LU2SemiU ⪯ SysF_TYP.
proof: Proof. exists (fun '(s, t0, t1) => (sval (Argument.HM_W2 s t0 t1))). move=> [[s t0] t1]. constructor. - exact: Argument.transport. - exact: Argument.inverse_transport. 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 Undecidability.Synthetic.Definitions