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

State before:
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
x : Unit → ℕ → Bool
⊢ eval neg x = negSeq (x ())
Tactic:
dsimp [neg, 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 =
    negSeq (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 =
    negSeq (x ())
Tactic:
rw [neg_eq_propagate]
State after:
no goals