exact ⟨p, h hp, rfl⟩
L : Language
inst✝ : L.ORing
C C' : Semiformula L ℕ 1 → Prop
h : ∀ {p : Semiformula L ℕ 1}, C p → C' p
p : Semiformula L ℕ 1
hp : C p
⊢ ∃ p_1, C' p_1 ∧ ∀ᶠ* succInd p = ∀ᶠ* succInd p_1
no goals