- Make sure that arguments to the lemmas are in the consistent order:
\Gamma, E1, E2, K, e1, e2, \tau -- from left to right, as you write it
 on paper
- Add masks to all the lemmas
- Add missing rules
- Remove unnecessary closedness conditions