case id [( id : term )] … [( id : term )]

The user must have started a proof by induction/cases that has not been concluded yet, id must be a constructor for the inductive type of the term under induction/case-analysis, and the case must not have already been proved.

It starts the proof for the case id, where id1:T1,…,idn:Tn are the arguments of the constructor, each declared with its type.

The sequent for the case id.