An exact proof term for the current goal is nat_ind p H1 (λn H _ ⇒ H2 n H).