proposition: Lemma exists_match_DecOpt {B} P {_ : DecOpt P} (k : nat -> G (option B)) z : DecOptSizeMonotonic P -> DecOptCompletePos P -> SizedMonotonicOpt k -> P -> (exists s, semProdOpt (k s) z) -> exists (s : nat), semProdOpt (match decOpt s.+1 with | Some true => k s | _ => returnGen None end) z.
proof: Proof. intros Hmon Hcom Hmonk Hp [s1 [s [_ He]]]. eapply Hcom in Hp. destruct Hp as [s2 Hdec]. eexists (max s1 s2). eapply Hmon in Hdec. rewrite Hdec. eexists. split. reflexivity. eapply Hmonk > [ | eassumption ]. ssromega. ssromega. 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)