proposition: Lemma FIB_HF1 b x : i_f b x <> i_e.
proof: Proof. destruct x as [ [s H]|]; cbn; try congruence. destruct le_dec; try congruence. injection. congruence. 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