unfold List.eraseIdx
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
b : List (HeapNodeAux α (Heap α))
id : ℕ
t : BinTree α
ts : List (HeapNodeAux α (Heap α))
st : IsSearchTree le t
mh : IsMinHeap le (Heap.heap ts)
⊢ IsMinHeap le (Heap.heap (List.eraseIdx (t :: ts) id))
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
b : List (HeapNodeAux α (Heap α))
id : ℕ
t : BinTree α
ts : List (HeapNodeAux α (Heap α))
st : IsSearchTree le t
mh : IsMinHeap le (Heap.heap ts)
⊢ IsMinHeap le
    (Heap.heap
      (match t :: ts, id with
      | [], x => []
      | head :: as, 0 => as
      | a :: as, Nat.succ n => a :: List.eraseIdx as n))