case id (id1:T1) … (idn:Tn)
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.