proposition: Theorem reduction : SysF_TYP ⪯ SysF_TC.
proof: Proof. exists (fun 'M0 => (Argument.Gamma_M0, Argument.M_M0 M0, Argument.t_M0)). move=> M0. constructor. - exact: Argument.transport. - exact: Argument.inverse_transport. 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 Undecidability.Synthetic.Definitions