the Simplification of the Induction Conclusion (Step 12)

Subgoal *1/2'
T

So, indeed, Subgoal *1/2' does simplify to T!

You can see that even in an example as simple as this one, quite a lot happens in simplification.

You may click here to return to the main proof.