simp only [Formula.primeSet] at h1
F' phi : Formula
phi_ih : F' ∈ phi.primeSet → F'.IsPrime
h1 : F' ∈ phi.not_.primeSet
⊢ F'.IsPrime
F' phi : Formula
phi_ih : F' ∈ phi.primeSet → F'.IsPrime
h1 : F' ∈ phi.primeSet
⊢ F'.IsPrime