ext m
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
n : ℕ
x : Fin (n + 1) → ℕ → Bool
⊢ eval (var n) x = x (Fin.last n)
case h
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
n : ℕ
x : Fin (n + 1) → ℕ → Bool
m : ℕ
⊢ eval (var n) x m = x (Fin.last n) m