have := calc
  true = (true && true) := rfl
  _    = (UInt.getBit x i && UInt.getBit y i) := by rw [hi i, decide_eq_true rfl, hyi]
  _    = UInt.getBit (x &&& y) i := by rw [UInt.getBit_land]
  _    = UInt.getBit (α:=α) 0 i := by rw [hcontra]
  _    = false := UInt.getBit_zero i
case a
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
i : Nat
x : α
hi : ∀ (j : Nat), UInt.getBit x j = decide (i = j)
f : Nat → α → α := fun i y => UInt.when (decide (x &&& bitmask (OfNat.ofNat i) ≠ 0)) (1 <<< OfNat.ofNat i) ||| y
this✝³ : UInt.getBit x i = true
this✝² : i < length α
this✝¹ : 0 < length α
foldf_high : ∀ (n k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
n : Nat
h_ind : n < length α → ∀ (k : Nat), k < n → UInt.getBit (Nat.fold f n 0) k = Nat.getBit i k
hn : Nat.succ n < length α
this✝ : n < length α
this : n < 2 ^ length α
y : α
hyi : UInt.getBit y i = true
hcontra : x &&& y = 0
⊢ False
case a
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
i : Nat
x : α
hi : ∀ (j : Nat), UInt.getBit x j = decide (i = j)
f : Nat → α → α := fun i y => UInt.when (decide (x &&& bitmask (OfNat.ofNat i) ≠ 0)) (1 <<< OfNat.ofNat i) ||| y
this✝⁴ : UInt.getBit x i = true
this✝³ : i < length α
this✝² : 0 < length α
foldf_high : ∀ (n k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
n : Nat
h_ind : n < length α → ∀ (k : Nat), k < n → UInt.getBit (Nat.fold f n 0) k = Nat.getBit i k
hn : Nat.succ n < length α
this✝¹ : n < length α
this✝ : n < 2 ^ length α
y : α
hyi : UInt.getBit y i = true
hcontra : x &&& y = 0
this : true = false
⊢ False