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