Theorem: lindenbaumExtensionExtends (Fine/SystemB/Lindenbaum.lean)

State before:
t : Th
Δ : Ctx
⊢ ↑t ⊆ lindenbaumExtension t Δ
Tactic:
intros f h₁
State after:
t : Th
Δ : Ctx
f : Form
h₁ : f ∈ ↑t
⊢ f ∈ lindenbaumExtension t Δ

State before:
t : Th
Δ : Ctx
f : Form
h₁ : f ∈ ↑t
⊢ f ∈ lindenbaumExtension t Δ
Tactic:
refine ⟨⟨0,0⟩,?_⟩
State after:
t : Th
Δ : Ctx
f : Form
h₁ : f ∈ ↑t
⊢ f ∈ lindenbaumSequence t Δ (0, 0)

State before:
t : Th
Δ : Ctx
f : Form
h₁ : f ∈ ↑t
⊢ f ∈ lindenbaumSequence t Δ (0, 0)
Tactic:
assumption
State after:
no goals