proposition: Lemma enumeratingOpt_sound_simpl A (e : E (option A)) ch s : enumeratingOpt e ch s = Some true -> exists x, ch x = Some true.
proof: Proof. unfold enumeratingOpt. generalize (Enumerators.run e s), false. clear. induction l; intros b 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