unfold combine
case a
α : Type u
le : α → α → Bool
a b : BinTree α
ha : IsBinTree a
hb : IsBinTree b
hab : a.rank = b.rank
⊢ IsRankedTree 1 (combine le a b).rank (nodes (combine le a b).children)
case a
α : Type u
le : α → α → Bool
a b : BinTree α
ha : IsBinTree a
hb : IsBinTree b
hab : a.rank = b.rank
⊢ IsRankedTree 1
    (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]) }).rank
    (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)