Popping out of an Inductive Proof

Recall that our induction scheme (click here to revisit it) had two cases, the induction step (Subgoal *1/2) and the base case (Subgoal *1/1). Both have been proved!