Proof of complete_nat_ind_with_y