rw [decr_eq_propagate]
α β α' β' : 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 =
    decrSeq (x ())
no goals