Comment by mehulashah

I wonder if after all that work, we might automatically reduce the proof and discover a simpler one that could have been included in the “margin”.