case nil =>
  simp
  cases rt
  constructor
  . assumption
  . constructor
  . assumption
α : 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])
no goals