exact pval_of_pval_nat_of_sigma_one hq h
case inr.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a✝ : ℕ
p✝ q✝ : Semiformula ℒₒᵣ Empty a✝
hp : Hierarchy 𝚺 1 p✝
hq : Hierarchy 𝚺 1 q✝
e : Fin a✝ → ℕ
h : (Semiformula.Evalbm ℕ e) q✝
⊢ (Semiformula.Evalbm M fun x => ↑(e x)) q✝
no goals