constructor
case cons
α : 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 : ℕ
a✝² : IsBinTree head✝
a✝¹ : head✝.rank = n
a✝ : IsRankedTree (n + 1) m tail✝
⊢ IsRankedTree n (m + 1) (head✝ :: tail✝ ++ [a])
case cons.a
α : 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 : ℕ
a✝² : IsBinTree head✝
a✝¹ : head✝.rank = n
a✝ : IsRankedTree (n + 1) m tail✝
⊢ head✝.rank = n

case cons.a
α : 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 : ℕ
a✝² : IsBinTree head✝
a✝¹ : head✝.rank = n
a✝ : IsRankedTree (n + 1) m tail✝
⊢ IsRankedTree (n + 1) (m + 1) (List.append tail✝ [a])

case cons.a
α : 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 : ℕ
a✝² : IsBinTree head✝
a✝¹ : head✝.rank = n
a✝ : IsRankedTree (n + 1) m tail✝
⊢ IsBinTree head✝