aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/ssrtest/caseview.v
blob: 108cf46a93b5315c2d8b75790d922c6cc2433d36 (plain)
1
2
3
4
Require Import ssreflect.

Lemma test (A B : Prop) : A /\ B -> True.
Proof. by case=> _ /id _. Qed.