Goal False. intuition match goal with | |- _ => idtac " foo" end.