## Stream: new members

### Topic: induction over nested sigma

#### ????? (Feb 13 2020 at 15:14):

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.

rcases

#### Kevin Buzzard (Feb 13 2020 at 15:25):

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

#### ????? (Feb 13 2020 at 17:24):

awesome, thanks!

Last updated: May 15 2021 at 23:13 UTC