we need to prove

we need to prove t1 (id) or equivalently t2


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.

New sequents to prove:

The stated one if id is provided