rintro (H | ⟨X, bX, Y, bY, H₀, Hₛ, ⟨u, hu, ne2, ppu, hX, hY⟩⟩)
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x y : M
⊢ Exponential x y →
    x = 0 ∧ y = 1 ∨
      ∃ X ≤ y ^ 4,
        ∃ Y ≤ y ^ 4, (1 = ext 4 X ∧ 2 = ext 4 Y) ∧ Seqₛ y X Y ∧ ∃ u ≤ y ^ 2, u ≠ 2 ∧ PPow2 u ∧ x = ext u X ∧ y = ext u Y
case inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x y : M
H : x = 0 ∧ y = 1
⊢ x = 0 ∧ y = 1 ∨
    ∃ X ≤ y ^ 4,
      ∃ Y ≤ y ^ 4, (1 = ext 4 X ∧ 2 = ext 4 Y) ∧ Seqₛ y X Y ∧ ∃ u ≤ y ^ 2, u ≠ 2 ∧ PPow2 u ∧ x = ext u X ∧ y = ext u Y

case inr.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x y X : M
bX : X ≤ y ^ 4
Y : M
bY : Y ≤ y ^ 4
H₀ : Seq₀ X Y
Hₛ : Seqₛ y X Y
u : M
hu : u ≤ y ^ 2
ne2 : u ≠ 2
ppu : PPow2 u
hX : ext u X = x
hY : ext u Y = y
⊢ x = 0 ∧ y = 1 ∨
    ∃ X ≤ y ^ 4,
      ∃ Y ≤ y ^ 4, (1 = ext 4 X ∧ 2 = ext 4 Y) ∧ Seqₛ y X Y ∧ ∃ u ≤ y ^ 2, u ≠ 2 ∧ PPow2 u ∧ x = ext u X ∧ y = ext u Y