we need to prove term [(id )] [ or equivalently term]

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.

The stated one if id is provided