constructor <;> try assumption
case cons
α : Sort ?u.14584
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
α✝ : Type u_1
t : BinTree α✝
ts : List (BinTree α✝)
hpos : t.rank > 0
a✝² : IsBinTree t
a✝¹ : r < t.rank
a✝ : IsHeapForest' t.rank ts
⊢ IsHeapForest' (t.rank - 1) (t :: ts)
case cons.a
α : Sort ?u.14584
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
α✝ : Type u_1
t : BinTree α✝
ts : List (BinTree α✝)
hpos : t.rank > 0
a✝² : IsBinTree t
a✝¹ : r < t.rank
a✝ : IsHeapForest' t.rank ts
⊢ t.rank - 1 < t.rank