proposition: Lemma enumerating_complete A (e : E A) {Hc : Correct A e} ch : (exists x, ch x = Some true) -> exists s, enumerating e ch s = Some true.
proof: Proof. intros [x Hch]. unfold enumerating. assert (Hin : semProd e x). { eapply Hc. reflexivity. } destruct Hin as [s [_ Hsem]]. simpl in *. unfold semEnumSize in *. exists s. revert Hsem. generalize (Enumerators.run e s), false. induction l; intros b Hin; inv Hin; simpl. - rewrite Hch. reflexivity. - destruct (ch a); eauto. destruct b0; eauto. Qed.
imports: Coq.Classes.Morphisms mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrnat) Sets Tactics Recdef List ZArith ZArith.Znat Arith Producer Generators Enumerators