use⟨-8, -21, -5⟩
case zero
a b c : ℤθ
⊢ ∃ φ, ↑(unit ^ 3 ^ (Nat.zero + 1)) = 1 + 3 ^ (Nat.zero + 1) * φ

case succ
a b c : ℤθ
n : ℕ
ih : ∃ φ, ↑(unit ^ 3 ^ (n + 1)) = 1 + 3 ^ (n + 1) * φ
⊢ ∃ φ, ↑(unit ^ 3 ^ (Nat.succ n + 1)) = 1 + 3 ^ (Nat.succ n + 1) * φ
case h
a b c : ℤθ
⊢ ↑(unit ^ 3 ^ (Nat.zero + 1)) = 1 + 3 ^ (Nat.zero + 1) * { f := -8, g := -21, h := -5 }

case succ
a b c : ℤθ
n : ℕ
ih : ∃ φ, ↑(unit ^ 3 ^ (n + 1)) = 1 + 3 ^ (n + 1) * φ
⊢ ∃ φ, ↑(unit ^ 3 ^ (Nat.succ n + 1)) = 1 + 3 ^ (Nat.succ n + 1) * φ