## Stream: general

### Topic: double cases

#### orlando (Apr 08 2020 at 18:30):

Hello, a Little question :

i have a property  truc : ∃ (s : S ) (u : U), blabla  it's possible obtain directly  s, u, hyp_blabla
for the moment i do 2 line :

cases truc with s h_s,
cases h_s with u hyp_blabla,


I'm sure this is possible but i don't remember :confused:

#### Kevin Buzzard (Apr 08 2020 at 18:30):

rcases truc with \<s, u, hyp\>

#### orlando (Apr 08 2020 at 18:32):

ohhh my bad : i use  rcases truc with ⟨s, u hyp⟩,  i forget the  ,  stupid me !!!

Thx Kevin !

#### Kevin Buzzard (Apr 08 2020 at 18:34):

I watched 20 undergraduates playing a preliminary version of the natural number game last year and they always forgot the comma :-)

Last updated: May 11 2021 at 12:15 UTC