Mem induction Scheme sigma1 iff

lemma mem_inductionScheme_sigma1_iff (φ : _root_.LO.FirstOrder.ArithmeticSemiformula ℕ 0) :    (∃ σ ∈ InductionScheme ℒₒᵣ (Arithmetic.Hierarchy 𝚺 1), φ = (σ : _root_.LO.FirstOrder.ArithmeticSemiformula ℕ 0))      ↔ ∃ ψ : _root_.LO.FirstOrder.ArithmeticSemiformula ℕ 1, Hierarchy 𝚺 1 ψ ∧ φ = (succInd ψ).univCl' := by  simp only [InductionScheme, Set.mem_setOf_eq]  constructor  · rintro ⟨σ, ⟨ψ, hψ, rfl⟩, rfl⟩    exact ⟨ψ, hψ, by simp [Semiformula.coe_univCl_eq_univCl']⟩  · rintro ⟨ψ, hψ, rfl⟩    exact ⟨Semiformula.univCl (succInd ψ), ⟨ψ, hψ, rfl⟩,      by simp [Semiformula.coe_univCl_eq_univCl']⟩