Thanks. Yeah, I remember playing through QED when I researched competition. It was a good game but didn't match my Advanced Graphics :)
Undoing a whole subtree sounds like a good idea, especially for the future first order version where proof trees are likely bigger.