proposition: Lemma bstring_eq n (s t : bstring n) : proj1_sig s = proj1_sig t <-> s = t.
proof: Proof. split; try now intros ->. destruct s as [s H1], t as [t H2]; cbn. intros ->. now rewrite (le_unique _ _ H1 H2). 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