intros ha hb hab
α : Type u
le : α → α → Bool
a b : BinTree α
⊢ IsBinTree a → IsBinTree b → a.rank = b.rank → IsBinTree (combine le a b)
α : Type u
le : α → α → Bool
a b : BinTree α
ha : IsBinTree a
hb : IsBinTree b
hab : a.rank = b.rank
⊢ IsBinTree (combine le a b)