proposition: Lemma blist_eqb_spec : forall l1 l2, l1 = l2 <-> blist_eqb l1 l2 = true.
proof: Proof. intros l1 l2. unfold blist_eqb. destruct (list_eqb_spec Bool.eqb_spec l1 l2); firstorder congruence. Qed.
imports: Undecidability.Synthetic(Definitions EnumerabilityFacts ListEnumerabilityFacts) Lia Undecidability.L(LProd LBool LNat LOptions) Undecidability.L.Datatypes.List(List_basics List_eqb List_extra List_nat)