proposition: Lemma exists_match_decOpt P {_ : DecOpt P} { _ : DecOptSizeMonotonic P } s1 k : decOpt s1 = Some true -> (exists s, k (max s1 s) = Some true) -> (exists (s : nat), match decOpt s with | Some true => k s | Some false => Some false | None => None end = Some true).
proof: Proof. intros. eapply exists_match; eauto. Qed.
imports: String List RoseTrees Show State Producer Generators Enumerators Classes DependentClasses Checker Decidability TacticsUtil Ltac2(Ltac2)