induction over nested sigma

Stream: new members

[?????]

If I have a term $t : \Sigma x:A. \Sigma y:B. C$, is there a tactic equivalent to the pattern match match t with <x,y,p> := ... end? I want to extract the components all at once instead of repeating the induction tactic.

[Patrick Massot]

rcases

[Kevin Buzzard]

more precisely rcases t with ⟨x, y, p⟩

[?????]

awesome, thanks!