cases Nat.eq_zero_or_pos (length α)
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
i : Nat
⊢ UInt.getBit 1 i = (decide (0 < length α) && decide (i = 0))
case inl
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
i : Nat
h✝ : length α = 0
⊢ UInt.getBit 1 i = (decide (0 < length α) && decide (i = 0))

case inr
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
i : Nat
h✝ : length α > 0
⊢ UInt.getBit 1 i = (decide (0 < length α) && decide (i = 0))