proposition: Lemma None_dec X (x : option X) : {x = None} + {x <> None}.
proof: Proof. destruct x; auto. right. discriminate. Qed.
imports: Lia Arith Undecidability.PCP.PCP Undecidability.PCP.Util.PCP_facts Undecidability.Synthetic.DecidabilityFacts Undecidability(FOL.Utils.FullSyntax) Undecidability(FOL.FSAT) Undecidability.Shared.ListAutomation