Theorem: composeUnary_eval (Lean4bits/lemmas.lean)

State before:
α β α' β' : Type
γ : β → Type
p : PropagateStruc Unit
t : Term
q : PropagateSolution t
x : Fin (arity t) → ℕ → Bool
⊢ PropagateStruc.eval (composeUnary p q) x = PropagateStruc.eval p fun x_1 => evalFin t x
Tactic:
rw [composeUnary, PropagateStruc.eval_compose, q.good]
State after:
α β α' β' : Type
γ : β → Type
p : PropagateStruc Unit
t : Term
q : PropagateSolution t
x : Fin (arity t) → ℕ → Bool
⊢ (PropagateStruc.eval p fun a => PropagateStruc.eval q.toPropagateStruc fun i => x (id i)) =
    PropagateStruc.eval p fun x_1 => PropagateStruc.eval q.toPropagateStruc x

State before:
α β α' β' : Type
γ : β → Type
p : PropagateStruc Unit
t : Term
q : PropagateSolution t
x : Fin (arity t) → ℕ → Bool
⊢ (PropagateStruc.eval p fun a => PropagateStruc.eval q.toPropagateStruc fun i => x (id i)) =
    PropagateStruc.eval p fun x_1 => PropagateStruc.eval q.toPropagateStruc x
Tactic:
rfl
State after:
no goals