proposition: Lemma exists_enum_tl A (g : nat -> E (option A)) (gs : nat -> list (E (option A))) x : (exists s, semProdOpt (enumerate (gs s)) x) -> exists s, semProdOpt (enumerate (g s :: gs s)) x.
proof: Proof. intros [s He]. exists s. eapply (@enumerate_correct_opt A). eapply (@enumerate_correct_opt A) in He. destruct He as [z [Hin Hsem]]. eexists. split. now right; eauto. eassumption. 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)