simp [h₀.2]
case pos
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
h₀ : Seq₀ X Y
hₛ : Seqₛ y X Y
IH : ∀ y_1 < 4, y_1 ≠ 2 → y_1 ≤ y ^ 2 → PPow2 y_1 → Pow2 (ext y_1 Y)
ne2 : 4 ≠ 2
hi : 4 ≤ y ^ 2
ppi : PPow2 4
⊢ Pow2 (ext 4 Y)
no goals