. dsimp
  cases hb
  apply IsMinTree_append
  repeat assumption
case a.«_@».Project.Main._hyg.2095.inl
α : Type u
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
a b : BinTree α
ha : IsSearchTree le a
hb : IsSearchTree le b
h✝ : le b.val a.val = true
⊢ IsMinTree le { val := b.val, rank := b.rank + 1, children := heap (nodes b.children ++ [a]) }.val
    (nodes { val := b.val, rank := b.rank + 1, children := heap (nodes b.children ++ [a]) }.children)

case a.«_@».Project.Main._hyg.2095.inr
α : Type u
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
a b : BinTree α
ha : IsSearchTree le a
hb : IsSearchTree le b
h✝ : ¬le b.val a.val = true
⊢ IsMinTree le { val := a.val, rank := a.rank + 1, children := heap (nodes a.children ++ [b]) }.val
    (nodes { val := a.val, rank := a.rank + 1, children := heap (nodes a.children ++ [b]) }.children)
case a.«_@».Project.Main._hyg.2095.inr
α : Type u
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
a b : BinTree α
ha : IsSearchTree le a
hb : IsSearchTree le b
h✝ : ¬le b.val a.val = true
⊢ IsMinTree le { val := a.val, rank := a.rank + 1, children := heap (nodes a.children ++ [b]) }.val
    (nodes { val := a.val, rank := a.rank + 1, children := heap (nodes a.children ++ [b]) }.children)