dsimp [sub, eval]
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
x : Bool → ℕ → Bool
⊢ eval sub x = subSeq (x true) (x false)
α β α' β' : Type
γ : β → Type
arity : Type
p : PropagateStruc arity
x : Bool → ℕ → Bool
⊢ propagate (fun x => false)
      (fun carry bits =>
        (fun x => !bits true && bits false || !_root_.xor (bits true) (bits false) && carry (),
          _root_.xor (bits true) (_root_.xor (bits false) (carry ()))))
      x =
    subSeq (x true) (x false)