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