I've been working on a similar project for high school algebra. Mine isn't as far along, so it's been nice to see some validation on my ideas, as well as get some thoughts on how I would improve.
How do you make contraction happen? I don't see a button for it.
We do contraction on implication-left automatically, and only have it as an option for forall-left and exists-right, since it's not a useful notion for the other operators.