Further proof construction improvements
Fix lfp

It should not leave junk in the proof tree when the strategy fails