case botC ih => apply botC; solve_by_elim [insert_subset_insert]
v : Variable → Prop
A B : Formula
Γ Γ✝ : Set Formula
A✝ : Formula
a✝ : insert (~A✝) Γ✝ ⊢ ⊥
ih : ∀ {Δ : Set Formula}, insert (~A✝) Γ✝ ⊆ Δ → Δ ⊢ ⊥
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝
no goals