case inl => exact Or.inr rfl
t : Th
Δ : Ctx
f g : Form
i j : ℕ
k : ℕ := Encodable.encode (f, g)
l₂ : f¦g ∈ lindenbaumSequence t Δ (i + 1, k)
prev : Ctx := lindenbaumSequence t Δ (i + 1, k)
l₄ : Denumerable.ofNat (Form × Form) k = (f, g)
h₁ : ▲(prev ∪ {f}) ∩ Δ = ∅
h✝ : f¦g ∈ ▲prev
⊢ f ∈ prev ∪ {f}
no goals