simp [propagateCarry, propagateCarry2_succ]
α β α' β' : Type
γ : β → Type
init_carry✝ : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
x : β → ℕ → Bool
init_carry : α → Bool
next_carr : (α → Bool) → (β → Bool) → α → Bool
n : ℕ
⊢ propagateCarry2 (propagateCarry2 init_carry next_carr x (n + 1)) next_carr (fun b k => x b (k + (n + 1))) 0 =
    propagateCarry2 init_carry next_carr x (0 + (n + 1))
no goals