{ erw [Nat.add_succ, propagate_succ2, propagate_succ2, Nat.add_eq, Nat.add_eq]
  simp [← Nat.succ_eq_add_one, ← Nat.add_succ, h₃ _ _ (le_refl _)]
  congr
  . apply propagateCarry2_eq_of_carry_eq
    . assumption
    . exact λ y b h => h₃ y b (Nat.le_succ_of_le h)
  . funext i
    rw [h₃]
    exact Nat.le_succ _ }
case succ
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq₁ seq₂ : β → ℕ → Bool
m n : ℕ
h₁ :
  propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₁ m =
    propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₂ n
n✝ : ℕ
h₃ : ∀ (y : ℕ) (b : β), y ≤ Nat.succ n✝ → seq₁ b (m + y) = seq₂ b (n + y)
⊢ propagate init_carry next_bit seq₁ (m + Nat.succ n✝) = propagate init_carry next_bit seq₂ (n + Nat.succ n✝)
no goals