Subgoal *1/1 is the Base Case of our induction. It simplifies to Subgoal *1/1' by expanding the ENDP term in the hypothesis, just as we saw in the earlier proof of Subgoal *1/2.

Subgoal *1/1

Subgoal *1/1'

Subgoal *1/2