intro
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
t₁ t₂ : BinTree α
⊢ t₁.rank = t₂.rank → (combine le t₁ t₂).rank = t₁.rank + 1
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
t₁ t₂ : BinTree α
a✝ : t₁.rank = t₂.rank
⊢ (combine le t₁ t₂).rank = t₁.rank + 1