case cons _ _ ih =>
  cases rt
  constructor
  . assumption
  . apply ih
    assumption
  . assumption
α : Type u
m : ℕ
α✝ : Type u_1
a : BinTree α✝
ha : IsBinTree a
hrank : a.rank = m
head✝ : BinTree α✝
tail✝ : List (BinTree α✝)
ih : ∀ {n : ℕ}, IsRankedTree n m tail✝ → IsRankedTree n (m + 1) (tail✝ ++ [a])
n : ℕ
rt : IsRankedTree n m (head✝ :: tail✝)
⊢ IsRankedTree n (m + 1) (head✝ :: tail✝ ++ [a])
no goals