induction xs with
| nil =>
  simp
  constructor <;> assumption
| cons _ _ ih => 
  cases h
  constructor
  . assumption
  . simp
    apply ih
    assumption
  . assumption
α : Type u
α✝ : Type u_1
le : α✝ → α✝ → Bool
m : α✝
xs : List (BinTree α✝)
a : BinTree α✝
h : IsMinTree le m xs
ha : IsSearchTree le a
hba : le m a.val = true
⊢ IsMinTree le m (xs ++ [a])
no goals