proposition: Lemma FIB_HF2' x y : i_f true x = i_f false y -> i_f true x = None /\ i_f false y = None.
proof: Proof. intros H. destruct (None_dec (i_f' true x)), (None_dec (i_f' false y)); try tauto; exfalso. all: unfold i_f'. - symmetry in H. specialize (FIB_HF2 n0 H). intros [H1 H2]; congruence. - specialize (FIB_HF2 n0 H). intros [H1 H2]; congruence. - specialize (FIB_HF2 n0 H). intros [_ H']. 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