ext n
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
x : Unit → ℕ → Bool
⊢ eval not x = notSeq (x ())
case h
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
x : Unit → ℕ → Bool
n : ℕ
⊢ eval not x n = notSeq (x ()) n