proposition: Lemma enumeratingOpt_sound A P (e : E (option A)) {Hc : CorrectST P e} ch s : enumeratingOpt e ch s = Some true -> exists x, P x /\ ch x = Some true.
proof: Proof. unfold enumeratingOpt. assert (Hs : forall x, LazyList.In_ll (Some x) (Enumerators.run e s) -> P x). { intros. eapply Hc. eexists. split; eauto. reflexivity. simpl. eassumption. } revert Hs. generalize (Enumerators.run e s), false. clear. induction l; intros b Hyp Heq; simpl in *. - destruct b; congruence. - destruct a; eauto. destruct (ch a) as [ [| ] | ] eqn:Heq'; eauto. Qed.
imports: String List mathcomp(ssreflect ssrfun ssrbool ssrnat eqtype seq) Producer Generators Enumerators Tactics Sets Classes