rw [toNat_land]
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x y : α
i : Nat
⊢ Nat.getBit (toNat (x &&& y)) i = (Nat.getBit (toNat x) i && Nat.getBit (toNat y) i)
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x y : α
i : Nat
⊢ Nat.getBit (toNat x &&& toNat y) i = (Nat.getBit (toNat x) i && Nat.getBit (toNat y) i)