match hf with 
| .nil =>
  constructor
| .cons (t := t) (ts := ts) lt _ _ =>
  rw[← heq] at lt
  have b : h₁.rank + 1 ≤ t.rank := by
    apply Nat.succ_le_of_lt lt
  rw[hrank_of_cons] at *
  constructor
  . unfold bne at *
    rw[Nat.not_beq_eq_true_eq] at *
    apply lt_of_le_of_ne <;> assumption
  repeat assumption
case inr.inr.inr.inl.hys.a.cons
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hxs : IsHeapForest' rx (h₁ :: t₁)
h✝³ : (h₁.rank + 1 != hRank t₂) = true
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
h✝ : (h₁.rank + 1 != hRank t₁) = false
heq : h₁.rank = h₂.rank
a✝¹ : IsBinTree h₂
a✝ : ry < h₂.rank
hf : IsHeapForest' h₂.rank t₂
⊢ IsHeapForest' (h₁.rank + 1) t₂
no goals