simp [addSeq, addSeqAux]
α β α' β' : Type
γ : β → Type
x y : ℕ → Bool
n : ℕ
⊢ addSeq x y 0 =
    propagate (fun x => false)
      (fun carry bits =>
        (fun x => bits true && bits false || bits false && carry () || bits true && carry (),
          _root_.xor (bits true) (_root_.xor (bits false) (carry ()))))
      (fun b => bif b then x else y) 0
no goals