. dsimp
  cases ha
  apply IsRankedTree_append
  repeat assumption
  simp_all
case a.«_@».Project.Main._hyg.1829.inr
α : Type u
le : α → α → Bool
a b : BinTree α
ha : IsBinTree a
hb : IsBinTree b
hab : a.rank = b.rank
h✝ : ¬le b.val a.val = true
⊢ IsRankedTree 1 { val := a.val, rank := a.rank + 1, children := heap (nodes a.children ++ [b]) }.rank
    (nodes { val := a.val, rank := a.rank + 1, children := heap (nodes a.children ++ [b]) }.children)
no goals