proposition: Lemma enumerating_sound A (e : E A) ch s : enumerating e ch s = Some true -> exists x, ch x = Some true.
proof: Proof. unfold enumerating. generalize (Enumerators.run e s), false. induction l; intros b Heq; simpl in *. - destruct b; congruence. - destruct (ch a) as [ [| ] | ] eqn:Heq'; eauto. Qed.
imports: ZArith List mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat) Numbers.BinNums Classes.RelationClasses ExtLib.Structures(Functor Applicative) QuickChick(Sets Tactics Producer LazyList RandomQC)