have := λ a b hab => (le_antisymm (h a b hab) (h b a hab.symm)).symm
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq : β → ℕ → Bool
this : DecidableEq α
h :
  ∀ (n m : Fin (2 ^ card α + 1)),
    propagateCarry2 init_carry next_carry seq ↑n = propagateCarry2 init_carry next_carry seq ↑m → m ≤ n
⊢ False
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq : β → ℕ → Bool
this✝ : DecidableEq α
h :
  ∀ (n m : Fin (2 ^ card α + 1)),
    propagateCarry2 init_carry next_carry seq ↑n = propagateCarry2 init_carry next_carry seq ↑m → m ≤ n
this :
  ∀ (a b : Fin (2 ^ card α + 1)),
    propagateCarry2 init_carry next_carry seq ↑a = propagateCarry2 init_carry next_carry seq ↑b → a = b
⊢ False