rw [pow_one]
case zero
a b c : ℤθ
⊢ ∃ a b c,
    (↑(unit ^ 3 ^ 1)).f = 1 + 3 ^ 1 + 3 ^ 2 * a ∧
      (↑(unit ^ 3 ^ 1)).g = 3 ^ 2 * b ∧ (↑(unit ^ 3 ^ 1)).h = 3 ^ 1 + 3 ^ 2 * c
case zero
a b c : ℤθ
⊢ ∃ a b c, (↑(unit ^ 3)).f = 1 + 3 ^ 1 + 3 ^ 2 * a ∧ (↑(unit ^ 3)).g = 3 ^ 2 * b ∧ (↑(unit ^ 3)).h = 3 ^ 1 + 3 ^ 2 * c