proposition: Lemma FIB_HP x y : i_P x y -> x <> None /\ y <> None.
proof: Proof. destruct x as [ [s HS] |], y as [ [t HT]|]; auto. intros _. split; 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