|
default. Interestingly, there is an example where it makes the rest of
the proof less natural.
Goal forall x y:Z, ...
intros [y|p1[|p2|p2]|p1[|p2|p2]].
where case analysis on y is not only in the 2nd and 3rd case, is not
anymore easy to do.
Still, I find the bracketing of intro-patterns a natural property, and
its generalization in all situations a natural expectation for
uniformity. So, what to do? The following is e.g. not as compact and
"one-shot":
intros [|p1|p1]; [intros y|intros [|p2|p2] ..].
|
