Replaced repetitive proof with tactic notation
Rewrote lemmatwo_3 proof with tactic notation
Added note.