Refactored the proof-reconstruction code a bit.
Extracted the MFOLE tactic out of the replace_subgoal_tac function.