induction n <;> simp [incrSeqAux, *]
α β α' β' : Type
γ : β → Type
x : ℕ → Bool
n : ℕ
⊢ (incrSeqAux x n).snd = propagateCarry (fun x => true) (fun carry bits x => bits () && carry ()) (fun x_1 => x) n ()
no goals