simp only [decide_eq_true hi, UInt.getBit_zero]
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
hi : i < length α
this : 0 - 1 = ~~~0
⊢ (UInt.getBit 0 i != decide (i < length α) && UInt.getBit a i) = UInt.getBit a i
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
hi : i < length α
this : 0 - 1 = ~~~0
⊢ (false != true && UInt.getBit a i) = UInt.getBit a i