constructor
α : 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 α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬(u.rank + 1 != hRank y) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
a✝⁴ : IsHeapForest' u.rank y
a✝³ : IsBinTree c
a✝² : r < c.rank
hf : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : c.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ¬u.rank + 1 = t.rank
hle : c.rank + 1 ≤ t.rank
⊢ IsHeapForest' (u.rank + 1) (t :: ts)
case a
α : 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 α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬(u.rank + 1 != hRank y) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
a✝⁴ : IsHeapForest' u.rank y
a✝³ : IsBinTree c
a✝² : r < c.rank
hf : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : c.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ¬u.rank + 1 = t.rank
hle : c.rank + 1 ≤ t.rank
⊢ u.rank + 1 < t.rank

case a
α : 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 α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬(u.rank + 1 != hRank y) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
a✝⁴ : IsHeapForest' u.rank y
a✝³ : IsBinTree c
a✝² : r < c.rank
hf : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : c.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ¬u.rank + 1 = t.rank
hle : c.rank + 1 ≤ t.rank
⊢ IsBinTree t

case a
α : 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 α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬(u.rank + 1 != hRank y) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
a✝⁴ : IsHeapForest' u.rank y
a✝³ : IsBinTree c
a✝² : r < c.rank
hf : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : c.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ¬u.rank + 1 = t.rank
hle : c.rank + 1 ≤ t.rank
⊢ IsHeapForest' t.rank ts