α : Type u_1
le : α → α → Bool
s : Heap α
⊢ NoSibling
    (match s with
    | h₁@h_1:(node a child h₂@h:(node a_1 child_1 s)) => merge le (merge le h₁ h₂) (combine le s)
    | h => h)
α : Type u_1
le : α → α → Bool
s : Heap α
⊢ NoSibling (combine le s)
unfold combine
case h_1
α : Type u_1
le : α → α → Bool
x✝ : Heap α
a✝¹ : α
child✝¹ : Heap α
a✝ : α
child✝ s✝ : Heap α
⊢ NoSibling (merge le (merge le (node a✝¹ child✝¹ (node a✝ child✝ s✝)) (node a✝ child✝ s✝)) (combine le s✝))

case h_2
α : Type u_1
le : α → α → Bool
s x✝¹ : Heap α
x✝ : ∀ (a : α) (child : Heap α) (a_1 : α) (child_1 s_1 : Heap α), s = node a child (node a_1 child_1 s_1) → False
⊢ NoSibling s
α : Type u_1
le : α → α → Bool
s : Heap α
⊢ NoSibling
    (match s with
    | h₁@h_1:(node a child h₂@h:(node a_1 child_1 s)) => merge le (merge le h₁ h₂) (combine le s)
    | h => h)
split
no goals
case h_1
α : Type u_1
le : α → α → Bool
x✝ : Heap α
a✝¹ : α
child✝¹ : Heap α
a✝ : α
child✝ s✝ : Heap α
⊢ NoSibling (merge le (merge le (node a✝¹ child✝¹ (node a✝ child✝ s✝)) (node a✝ child✝ s✝)) (combine le s✝))
exact noSibling_merge _ _ _
no goals
case h_2
α : Type u_1
le : α → α → Bool
s x✝¹ : Heap α
x✝ : ∀ (a : α) (child : Heap α) (a_1 : α) (child_1 s_1 : Heap α), s = node a child (node a_1 child_1 s_1) → False
⊢ NoSibling s
match s with
| nil | node _ _ nil => constructor
| node _ _ (node _ _ s) => rename_i h; exact (h _ _ _ _ _ rfl).elim
no goals
α : Type u_1
le : α → α → Bool
s x✝¹ : Heap α
a✝ : α
child✝ : Heap α
x✝ :
  ∀ (a : α) (child : Heap α) (a_1 : α) (child_1 s : Heap α),
    node a✝ child✝ nil = node a child (node a_1 child_1 s) → False
⊢ NoSibling (node a✝ child✝ nil)
constructor
α : Type u_1
le : α → α → Bool
s✝ x✝ : Heap α
a✝¹ : α
child✝¹ : Heap α
a✝ : α
child✝ s : Heap α
h :
  ∀ (a : α) (child : Heap α) (a_1 : α) (child_1 s_1 : Heap α),
    node a✝¹ child✝¹ (node a✝ child✝ s) = node a child (node a_1 child_1 s_1) → False
⊢ NoSibling (node a✝¹ child✝¹ (node a✝ child✝ s))
α : Type u_1
le : α → α → Bool
s✝ x✝¹ : Heap α
a✝¹ : α
child✝¹ : Heap α
a✝ : α
child✝ s : Heap α
x✝ :
  ∀ (a : α) (child : Heap α) (a_1 : α) (child_1 s_1 : Heap α),
    node a✝¹ child✝¹ (node a✝ child✝ s) = node a child (node a_1 child_1 s_1) → False
⊢ NoSibling (node a✝¹ child✝¹ (node a✝ child✝ s))
rename_i h
no goals
α : Type u_1
le : α → α → Bool
s✝ x✝ : Heap α
a✝¹ : α
child✝¹ : Heap α
a✝ : α
child✝ s : Heap α
h :
  ∀ (a : α) (child : Heap α) (a_1 : α) (child_1 s_1 : Heap α),
    node a✝¹ child✝¹ (node a✝ child✝ s) = node a child (node a_1 child_1 s_1) → False
⊢ NoSibling (node a✝¹ child✝¹ (node a✝ child✝ s))
exact (h _ _ _ _ _ rfl).elim