Intro pattern

[Rocq] A tactic modifier in Rocq:(/programming-language-theory/concepts/rocq) that destructures hypothesises as they're introduced (like intros [x y] to unpack a pair or intros [H|H] for a disjunction).