Theorem: PropagateStruc.eval_var (Lean4bits/lemmas.lean)

State before:
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
n : ℕ
x : Fin (n + 1) → ℕ → Bool
⊢ eval (var n) x = x (Fin.last n)
Tactic:
ext m
State after:
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

State before:
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
Tactic:
cases m <;> simp [var, eval, propagate_succ]
State after:
no goals