proposition: Theorem reduction : H10C_SAT ⪯ SysF_INH.
proof: Proof. exists (fun h10cs => (Argument.GammaH h10cs, poly_var Argument.tt)). move=> h10cs. constructor. - exact: Argument.transport. - exact: Argument.inverse_transport. Qed.
imports: PeanoNat List Lia Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Util(Facts poly_type_facts term_facts typing_facts iipc2_facts sn_facts) Undecidability.DiophantineConstraints.H10C ssreflect ssrbool ssrfun Undecidability.Synthetic.Definitions