intros h₂
case h
Γ : Pr
f : Form
h₁ : f ∈ ↑↑(primeStarFunction (primeStarFunction Γ))
⊢ ¬f ∈ ↑↑Γ → False
case h
Γ : Pr
f : Form
h₁ : f ∈ ↑↑(primeStarFunction (primeStarFunction Γ))
h₂ : ¬f ∈ ↑↑Γ
⊢ False