cases n <;> simp [one, oneSeq, eval, propagate_succ2, @eq_comm _ false]
case h
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
x : Fin 0 → ℕ → Bool
n : ℕ
⊢ eval one x n = oneSeq n
no goals