case id (id1:t1) … (idn:tn)
- Synopsis:
case id [( id : term )] …
- Pre-condition:
To be used in a proof by induction or by cases to start
a new case
- Action:
Starts the new case id declaring
the local parameters (id1:t1) … (idn:tn)
- New sequents to prove:
None
Matita Home