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