unfold mergeNodes
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
h : List (BinTree α)
⊢ mergeNodes le [] h = h
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
h : List (BinTree α)
⊢ (match [], h with
    | [], h => h
    | h, [] => h
    | f@h:(h₁ :: t₁), s@h_1:(h₂ :: t₂) =>
      if h₁.rank < h₂.rank then h₁ :: mergeNodes le t₁ s
      else
        if h₂.rank < h₁.rank then h₂ :: mergeNodes le t₂ f
        else
          let merged := combine le h₁ h₂;
          let r := merged.rank;
          if (r != hRank t₁) = true then
            if (r != hRank t₂) = true then merged :: mergeNodes le t₁ t₂ else mergeNodes le (merged :: t₁) t₂
          else if (r != hRank t₂) = true then mergeNodes le t₁ (merged :: t₂) else merged :: mergeNodes le t₁ t₂) =
    h