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 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.