proposition: Lemma checker_backtrack_spec_exists (l : nat -> list (unit -> option bool)) : (exists (f : nat -> (unit -> option bool)), (forall s, List.In (f s) (l s)) /\ exists s, f s tt = Some true) -> exists s, checker_backtrack (l s) = Some true.
proof: Proof. intros [f [Hall [s Heq]]]. eexists s. eapply checker_backtrack_spec. eexists. split; eauto. Qed.
imports: String List RoseTrees Show State Producer Generators Enumerators Classes DependentClasses Checker Decidability TacticsUtil Ltac2(Ltac2)