Require Import ssreflect.
Goal forall p : nat * nat , True.
case => x x.
Abort.