match n with
| 0 => simp [addSeq, addSeqAux]
| 1 => simp [addSeq, addSeqAux, propagate, propagateAux]
| n+2 => simp [addSeq, addSeqAux, addSeqAux_eq_propagateCarry, propagate_succ]
case h
α β α' β' : Type
γ : β → Type
x y : ℕ → Bool
n : ℕ
⊢ addSeq x y n =
    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) n
no goals