{ cases n
  { simp [*, propagate_succ2] at *
    have := fun i => h₃ 0 i rfl
    dsimp at this
    simp [this]
    simp [h₁] }
  { rw [propagate_succ2, h₁, propagate_succ2]
    have := h₃ 0
    simp [*] at * } }
case zero.succ
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq₁ seq₂ : β → ℕ → Bool
n n✝ : ℕ
h₁ :
  propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₁ (Nat.succ n✝) =
    propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₂ n
h₃ : ∀ (y : ℕ) (b : β), y ≤ Nat.zero → seq₁ b (Nat.succ n✝ + y) = seq₂ b (n + y)
⊢ propagate init_carry next_bit seq₁ (Nat.succ n✝ + Nat.zero) = propagate init_carry next_bit seq₂ (n + Nat.zero)
no goals