proposition: Lemma reflect_decOpt (P : Prop) {Hd : Dec P} {Hm : DecOptSizeMonotonic P} {Hc : DecOptCompletePos P} {Hs : DecOptCorrectPos P} s b : decOpt s = Some b -> Bool.reflect P b.
proof: Proof. intros Heq. destruct b. - constructor. eapply Hs. eassumption. - constructor. intros HP. eapply decOptSoundNeg in Heq; now eauto. Qed.
imports: String List RoseTrees Show State Producer Generators Enumerators Classes DependentClasses Checker Decidability TacticsUtil Ltac2(Ltac2)