Sometimes when proving things (e.g. when proving the second lemma for Homework #2), you will get to the point where the thing you need to prove is already available, say as d2. Then you can write:
... by d2In SASyLF before version 12, this would be accepted in all cases. Make sure you use a recent SASyLF to check your work.
If you write the lemma (3) in the obvious way, you will find the lemma useless. The problem is that if variables (such as t2 and t3) occur only in the exists then SASyLF treats them as existentially quantified. Since that would make the lemma useless (think about it), you need to explicitly make them forall variables. The lemma will thus have three inputs.