. simp
  apply ih
  assumption
case cons.cons.a
α : Type u
α✝ : Type u_1
le : α✝ → α✝ → Bool
m : α✝
a : BinTree α✝
ha : IsSearchTree le a
hba : le m a.val = true
head✝ : BinTree α✝
tail✝ : List (BinTree α✝)
ih : IsMinTree le m tail✝ → IsMinTree le m (tail✝ ++ [a])
a✝² : IsSearchTree le head✝
a✝¹ : le m head✝.val = true
a✝ : IsMinTree le m tail✝
⊢ IsMinTree le m (List.append tail✝ [a])

case cons.cons.a
α : Type u
α✝ : Type u_1
le : α✝ → α✝ → Bool
m : α✝
a : BinTree α✝
ha : IsSearchTree le a
hba : le m a.val = true
head✝ : BinTree α✝
tail✝ : List (BinTree α✝)
ih : IsMinTree le m tail✝ → IsMinTree le m (tail✝ ++ [a])
a✝² : IsSearchTree le head✝
a✝¹ : le m head✝.val = true
a✝ : IsMinTree le m tail✝
⊢ IsSearchTree le head✝
case cons.cons.a
α : Type u
α✝ : Type u_1
le : α✝ → α✝ → Bool
m : α✝
a : BinTree α✝
ha : IsSearchTree le a
hba : le m a.val = true
head✝ : BinTree α✝
tail✝ : List (BinTree α✝)
ih : IsMinTree le m tail✝ → IsMinTree le m (tail✝ ++ [a])
a✝² : IsSearchTree le head✝
a✝¹ : le m head✝.val = true
a✝ : IsMinTree le m tail✝
⊢ IsSearchTree le head✝