rw [propagateCarry2, propagateCarry2_succ _ _ _ n, propagateCarry]
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → α → Bool
x : β → ℕ → Bool
n : ℕ
⊢ propagateCarry2 init_carry next_bit x (n + 1 + 1) = propagateCarry init_carry next_bit x (n + 1)
no goals