Theorem: evalFin_eq_eval (Lean4bits/lemmas.lean)

State before:
α β α' β' : Type
γ : β → Type
t : Term
vars : ℕ → ℕ → Bool
⊢ (evalFin t fun i => vars ↑i) = eval t vars
Tactic:
induction t <;>
dsimp [Term.evalFin, Term.eval, arity] at * <;> simp [*]
State after:
no goals