case ax g h₁ => 
  let Gsing : Finset Form := {g} 
  have l₁ : g ∈ {g} := Finset.mem_singleton.mpr rfl
  have l₂ : Gsing = ({g} : Ctx) := Finset.coe_singleton g
  have l₃ : ↑Gsing ⊆ Γ := by
    intros g' h₂
    rw [l₂] at h₂
    rw [h₂]
    assumption
  have prf₂ : BProof ↑{g} g := by
    rw [←l₂]
    apply ax l₁
  rw [←l₂] at prf₂
  exact ⟨Gsing, l₃, prf₂⟩
Γ : Ctx
f g : Form
h₁ : g ∈ Γ
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) g
no goals