cases hel
α : 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
t : BinTree α
ts : List (BinTree α)
idx : ℕ
h' : BinTree α
idx' : ℕ
hle : le (findMin le (t :: ts) idx (h', idx')).fst.val h'.val = true
t₂ : BinTree α
hel : t₂ ∈ t :: ts
⊢ le (findMin le (t :: ts) idx (h', idx')).fst.val t₂.val = true
case head
α : 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
t : BinTree α
ts : List (BinTree α)
idx : ℕ
h' : BinTree α
idx' : ℕ
hle : le (findMin le (t :: ts) idx (h', idx')).fst.val h'.val = true
⊢ le (findMin le (t :: ts) idx (h', idx')).fst.val t.val = true

case tail
α : 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
t : BinTree α
ts : List (BinTree α)
idx : ℕ
h' : BinTree α
idx' : ℕ
hle : le (findMin le (t :: ts) idx (h', idx')).fst.val h'.val = true
t₂ : BinTree α
a✝ : List.Mem t₂ ts
⊢ le (findMin le (t :: ts) idx (h', idx')).fst.val t₂.val = true