α : Type u_1
le : α → α → Bool
s : Heap α
⊢ NoSibling (Option.getD (tail? le s) nil)
α : Type u_1
le : α → α → Bool
s : Heap α
⊢ NoSibling (tail le s)
simp only [Heap.tail]
no goals
α : Type u_1
le : α → α → Bool
s : Heap α
⊢ NoSibling (Option.getD (tail? le s) nil)
match eq : s.tail? le with
| none => cases s with cases eq | nil => constructor
| some tl => exact Heap.noSibling_tail? eq
no goals
α : Type u_1
le : α → α → Bool
s : Heap α
eq : tail? le s = none
⊢ NoSibling (Option.getD none nil)
cases s with cases eq | nil => constructor
no goals
case nil.refl
α : Type u_1
le : α → α → Bool
⊢ NoSibling (Option.getD none nil)
constructor
no goals
α : Type u_1
le : α → α → Bool
s tl : Heap α
eq : tail? le s = some tl
⊢ NoSibling (Option.getD (some tl) nil)
exact Heap.noSibling_tail? eq