unfold combine
case a
α : 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
⊢ IsMinTree le (combine le a b).val (nodes (combine le a b).children)
case a
α : 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
⊢ IsMinTree le
    (if le b.val a.val = true then { val := b.val, rank := b.rank + 1, children := heap (nodes b.children ++ [a]) }
      else { val := a.val, rank := a.rank + 1, children := heap (nodes a.children ++ [b]) }).val
    (nodes
      (if le b.val a.val = true then { val := b.val, rank := b.rank + 1, children := heap (nodes b.children ++ [a]) }
        else { val := a.val, rank := a.rank + 1, children := heap (nodes a.children ++ [b]) }).children)