induction xs generalizing n
α : Type u
n m : ℕ
α✝ : Type u_1
xs : List (BinTree α✝)
a : BinTree α✝
rt : IsRankedTree n m xs
ha : IsBinTree a
hrank : a.rank = m
⊢ IsRankedTree n (m + 1) (xs ++ [a])
case nil
α : 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 cons
α : Type u
m : ℕ
α✝ : Type u_1
a : BinTree α✝
ha : IsBinTree a
hrank : a.rank = m
head✝ : BinTree α✝
tail✝ : List (BinTree α✝)
tail_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])