induction n
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i n : Nat
⊢ i ∈ bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true
case zero
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
⊢ i ∈ bitIndices.aux a Nat.zero ↔ i < Nat.zero ∧ UInt.getBit a i = true

case succ
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i n✝ : Nat
n_ih✝ : i ∈ bitIndices.aux a n✝ ↔ i < n✝ ∧ UInt.getBit a i = true
⊢ i ∈ bitIndices.aux a (Nat.succ n✝) ↔ i < Nat.succ n✝ ∧ UInt.getBit a i = true