constructor
α : Type u
α✝ : Type u_1
a : α✝
⊢ IsHeap (singleton a)
case a
α : Type u
α✝ : Type u_1
a : α✝
⊢ 0 < { val := a, rank := 1, children := heap [] }.rank

case a
α : Type u
α✝ : Type u_1
a : α✝
⊢ IsBinTree { val := a, rank := 1, children := heap [] }

case a
α : Type u
α✝ : Type u_1
a : α✝
⊢ IsHeapForest' { val := a, rank := 1, children := heap [] }.rank []