simp at *
case inr.inr.inr.inl.hys.a.cons.cons
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
h✝³ : ¬h₁.rank < h₂.rank
h✝² : ¬h₂.rank < h₁.rank
h✝¹ : ¬((combine le h₁ h₂).rank != hRank t₁) = true
h✝ : ((combine le h₁ h₂).rank != hRank t₂) = true
a✝⁵ : IsBinTree h₁
a✝⁴ : rx < h₁.rank
a✝³ : IsHeapForest' h₁.rank t₁
a✝² : IsBinTree h₂
a✝¹ : ry < h₂.rank
a✝ : IsHeapForest' h₂.rank t₂
⊢ IsBinTree (combine le h₁ h₂)
case inr.inr.inr.inl.hys.a.cons.cons
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
h✝³ : ((combine le h₁ h₂).rank != hRank t₂) = true
a✝⁵ : IsBinTree h₁
a✝⁴ : rx < h₁.rank
a✝³ : IsHeapForest' h₁.rank t₁
a✝² : IsBinTree h₂
a✝¹ : ry < h₂.rank
a✝ : IsHeapForest' h₂.rank 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
⊢ IsBinTree (combine le h₁ h₂)