have ⟨prf₁⟩ := h₁
t : Th
Δ : Ctx
f : Form
h₁ : lindenbaumExtension t Δ⊢f
⊢ f ∈ lindenbaumExtension t Δ
t : Th
Δ : Ctx
f : Form
h₁ : lindenbaumExtension t Δ⊢f
prf₁ : BProof (lindenbaumExtension t Δ) f
⊢ f ∈ lindenbaumExtension t Δ