proposition: Lemma exists_match' check k s1 : check s1 = Some true -> (forall s1 s2, (s1 <= s2) -> check s1 = Some true -> check s2 = Some true) -> (forall s1 s2, (s1 <= s2) -> k s1 = Some true -> k s2 = Some true) -> (exists s, k s = Some true) -> (exists (s : nat) , match check s with | Some true => k s | Some false => Some false | None => None end = Some true).
proof: Proof. intros Hch Hmon Hmon' Hk. destruct Hk as [s2 Hk]. eexists (max s1 s2). erewrite Hmon > [ | | eassumption ]. eapply Hmon' > [ | eassumption ]. lia. lia. Qed.
imports: String List RoseTrees Show State Producer Generators Enumerators Classes DependentClasses Checker Decidability TacticsUtil Ltac2(Ltac2)