rw [propagateAux, propagateCarry, propagateAux_fst_eq_carry _ _ _ n]
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
x : β → ℕ → Bool
n : ℕ
⊢ (propagateAux init_carry next_bit x (n + 1)).fst = propagateCarry init_carry (fun c b => (next_bit c b).fst) x (n + 1)
no goals