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

State before:
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
x : Unit → ℕ → Bool
⊢ eval incr x = incrSeq (x ())
Tactic:
dsimp [incr, eval]
State after:
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
x : Unit → ℕ → Bool
⊢ propagate (fun x => true) (fun carry bits => (fun x => bits () && carry (), _root_.xor (bits ()) (carry ()))) x =
    incrSeq (x ())

State before:
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
x : Unit → ℕ → Bool
⊢ propagate (fun x => true) (fun carry bits => (fun x => bits () && carry (), _root_.xor (bits ()) (carry ()))) x =
    incrSeq (x ())
Tactic:
rw [incr_eq_propagate]
State after:
no goals