case a.a.h.mp =>
  apply byContradiction
  intros h₂
  have l₂ : ¬(~~f ∈ Γ) := h₂ ∘ λel => Γ.val.property.mpr ⟨BProof.mp (BProof.ax el) BTheorem.dne⟩
  exact h₁ l₂
Γ : Pr
f : Form
h₁ : f ∈ ↑↑(primeStarFunction (primeStarFunction Γ))
⊢ f ∈ ↑↑Γ
no goals