cases n <;> simp [xor, xorSeq, eval, propagate_succ]
case h
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
x : Bool → ℕ → Bool
n : ℕ
⊢ eval xor x n = xorSeq (x true) (x false) n
no goals