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