proposition: Lemma obstring_eqdec n : eq_dec (obstring n).
proof: Proof. apply option_eq_dec. unfold bstring. intros [a Ha] [b Hb]. destruct (list_eq_dec bool_eq_dec a b) as [Hn0|Hn0]. - subst. left. apply EqdepFacts.eq_dep_eq_sig. assert (Ha = Hb) as -> by (apply le_unique). constructor. - right. intros H. eapply Hn0, EqdepFacts.eq_sig_fst. exact H. Defined.
imports: Lia Arith Undecidability.PCP.PCP Undecidability.PCP.Util.PCP_facts Undecidability.Synthetic.DecidabilityFacts Undecidability(FOL.Utils.FullSyntax) Undecidability(FOL.FSAT) Undecidability.Shared.ListAutomation