rfl
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
x : β → ℕ → Bool
i : ℕ
⊢ propagate init_carry next_bit x (i + 1) =
    (next_bit (propagateAux init_carry (fun c b => next_bit c b) x i).fst fun j => x j (i + 1)).snd
no goals