rw [UInt.ofBool_true, this, UInt.getBit_land, UInt.getBit_complement]
case a
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a : α
i : Nat
hi : i < length α
this : 0 - 1 = ~~~0
⊢ UInt.getBit (0 - ofBool true &&& 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
⊢ (UInt.getBit 0 i != decide (i < length α) && UInt.getBit a i) = UInt.getBit a i