simp only [propagate_succ2, propagate_succ2, h _ _ (le_refl _)]
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
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
n✝ : ℕ
h : ∀ (b : β) (j : ℕ), j ≤ Nat.succ n✝ → seq₁ b j = seq₂ b j
⊢ propagate init_carry next_bit seq₁ (Nat.succ n✝) = propagate init_carry next_bit seq₂ (Nat.succ n✝)
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
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
n✝ : ℕ
h : ∀ (b : β) (j : ℕ), j ≤ Nat.succ n✝ → seq₁ b j = seq₂ b j
⊢ (next_bit (propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq₁ (n✝ + 1)) fun j =>
        seq₂ j (Nat.succ n✝)).snd =
    (next_bit (propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq₂ (n✝ + 1)) fun j => seq₂ j (n✝ + 1)).snd