suffices ∀ (n : Nat), i ∈ UInt.bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true by 
  constructor
  case mp => intro h; exact ((this (length α)).mp h).right
  case mpr =>
    intro h
    have hi : i < length α :=
      (Nat.lt_or_ge i (length α)).elim id (λ hi => by cases (UInt.getBit_high a i hi ▸ h))
    exact (this (length α)).mpr ⟨hi, h⟩
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
⊢ i ∈ UInt.bitIndices a ↔ UInt.getBit a i = true
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
⊢ ∀ (n : Nat), i ∈ bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true