cases ht₂ with  | cons _ _ hf =>
  match hf with
  | .nil =>
    constructor
  | .cons (t := t) (ts := ts) lt _ _ =>
    rename_i neq
    rw[rank_combine heq, hrank_of_cons] at *
    unfold bne at neq
    rw[Nat.not_beq_eq_true_eq] at neq
    have hle : c.rank + 1 ≤ t.rank := by
      apply Nat.succ_le_of_lt lt
    constructor
    . rw[← heq] at hle
      apply lt_of_le_of_ne <;> assumption
    . assumption
    . assumption
case a.cons
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ¬((combine le u c).rank != hRank y) = true
h✝ : ((combine le u c).rank != hRank z) = true
a✝² : IsBinTree u
a✝¹ : r < u.rank
a✝ : IsHeapForest' u.rank y
⊢ IsHeapForest' (combine le u c).rank z
no goals