proposition: Lemma bstring_eq' n (s t : bstring n) : proj1_sig s = proj1_sig t -> s = t.
proof: Proof. 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