proposition: Lemma destruct_match_false_l (check b : option bool): match check with | Some false => b | Some true => Some false | None => None end = Some true -> check = Some false /\ b = Some true.
proof: Proof. intros H. destruct check as [ [ | ] | ]; eauto; discriminate. Qed.
imports: String List RoseTrees Show State Producer Generators Enumerators Classes DependentClasses Checker Decidability TacticsUtil Ltac2(Ltac2)