Change arrows, again
Swap \in expressions round
fix notation for simp of plus
Down arrow for eval
Fix premise for [T-Lam]