apply Iff.intro
case a.a.h
Γ : Pr
f : Form
⊢ f ∈ ↑↑(primeStarFunction (primeStarFunction Γ)) ↔ f ∈ ↑↑Γ
case a.a.h.mp
Γ : Pr
f : Form
⊢ f ∈ ↑↑(primeStarFunction (primeStarFunction Γ)) → f ∈ ↑↑Γ

case a.a.h.mpr
Γ : Pr
f : Form
⊢ f ∈ ↑↑Γ → f ∈ ↑↑(primeStarFunction (primeStarFunction Γ))