Theorem: LO.FirstOrder.Arith.Theory.mem_indScheme_of_mem (Arithmetization/Basic/Ind.lean)

State before:
L : Language
inst✝ : L.ORing
C C' : Semiformula L ℕ 1 → Prop
p : Semiformula L ℕ 1
hp : C p
⊢ ∀ᶠ* succInd p ∈ indScheme L C
Tactic:
simp [indScheme]
State after:
L : Language
inst✝ : L.ORing
C C' : Semiformula L ℕ 1 → Prop
p : Semiformula L ℕ 1
hp : C p
⊢ ∃ p_1, C p_1 ∧ ∀ᶠ* succInd p = ∀ᶠ* succInd p_1

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