proposition: Lemma exists_return_Opt A (x : A) : exists s : nat, semProdOpt (returnEnum (Some x)) x.
proof: Proof. exists 0. eapply (@semReturn E _ ProducerSemanticsEnum); reflexivity. Qed.
imports: String micromega.Lia List Tactics TacticsUtil Instances Classes DependentClasses Sets Producer Enumerators Checker Decidability CheckerProofs Ltac2(Ltac2) mathcomp(ssreflect ssrfun ssrbool ssrnat eqtype seq)