cases rt
α : Type u
m : ℕ
α✝ : Type u_1
a : BinTree α✝
ha : IsBinTree a
hrank : a.rank = m
n : ℕ
rt : IsRankedTree n m []
⊢ IsRankedTree n (m + 1) [a]
case nil
α : Type u
m : ℕ
α✝ : Type u_1
a : BinTree α✝
ha : IsBinTree a
hrank : a.rank = m
⊢ IsRankedTree m (m + 1) [a]