proposition: Lemma FIB_HF2 b1 b2 x y : i_f b1 x <> None -> i_f b1 x = i_f b2 y -> x = y /\ b1 = b2.
proof: Proof. destruct x as [ [s HS] |], y as [ [t HT]|]; cbn. all: repeat destruct le_dec; cbn. all: try congruence. intros _ [= -> ->]. split; trivial. f_equal. now apply bstring_eq. 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