all_goals intros h₁
case a.a.h.mp
Γ : Pr
f : Form
⊢ f ∈ ↑↑(primeStarFunction (primeStarFunction Γ)) → f ∈ ↑↑Γ

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

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