case true =>
  simp
  constructor
  . intro h
    cases h
    case inl h => cases h; exact ⟨i.lt_succ_self, hbit⟩
    case inr h => exact ⟨Nat.le.step (h_ind.mp h).left, (h_ind.mp h).right⟩
  . intro h
    cases (Nat.lt_or_eq_of_le (Nat.le_of_lt_succ h.left))
    case inl hlt => exact Or.inr (h_ind.mpr ⟨hlt, h.right⟩)
    case inr heq => cases heq; exact Or.inl rfl
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i n : Nat
h_ind : i ∈ bitIndices.aux a n ↔ i < n ∧ UInt.getBit a i = true
hbit : UInt.getBit a n = true
⊢ (i ∈ if true = true then n :: bitIndices.aux a n else bitIndices.aux a n) ↔ i < Nat.succ n ∧ UInt.getBit a i = true
no goals