calc
  UInt.getBit (α:=α) 1 i
    = UInt.getBit (α:=α) 0 i := by rw [UInt.eq_of_length_eq_zero hzero 1 0]
  _ = false := UInt.getBit_zero i
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
i : Nat
hzero : length α = 0
⊢ UInt.getBit 1 i = false
no goals