Create empty boxes of formulas instead of asking for the missing parts upfront

[joom]

Currently the system asks for inputs upfront for rules like cut in LK, or Cons in Hoare logic. It could be better if when you apply these rules you get empty boxes instead, and you can fill the boxes in place.

This might require a different mode, I'm not sure yet.