Matita Home

`we need to prove t1 (id) or equivalently t2`

- Synopsis:
- Pre-condition:
- Action:
If

**id**is provided, starts a subproof that once concluded will be named**id**. Otherwise states what needs to be proved. If**t2**is provided, the new goal is immediately changed to**t2**wich must be equivalent to**t1**.- New sequents to prove:
The stated one if

**id**is provided