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