α : Type u_1
le : α → α → Bool
s₁ s₂ : Heap α
⊢ NoSibling
    (match s₁, s₂ with
    | nil, nil => nil
    | nil, node a₂ c₂ sibling => node a₂ c₂ nil
    | node a₁ c₁ sibling, nil => node a₁ c₁ nil
    | node a₁ c₁ sibling, node a₂ c₂ sibling_1 =>
      if le a₁ a₂ = true then node a₁ (node a₂ c₂ c₁) nil else node a₂ (node a₁ c₁ c₂) nil)
α : Type u_1
le : α → α → Bool
s₁ s₂ : Heap α
⊢ NoSibling (merge le s₁ s₂)
unfold merge
no goals
α : Type u_1
le : α → α → Bool
s₁ s₂ : Heap α
⊢ NoSibling
    (match s₁, s₂ with
    | nil, nil => nil
    | nil, node a₂ c₂ sibling => node a₂ c₂ nil
    | node a₁ c₁ sibling, nil => node a₁ c₁ nil
    | node a₁ c₁ sibling, node a₂ c₂ sibling_1 =>
      if le a₁ a₂ = true then node a₁ (node a₂ c₂ c₁) nil else node a₂ (node a₁ c₁ c₂) nil)
(split <;> try split) <;> constructor
case h_1
α : Type u_1
le : α → α → Bool
x✝¹ x✝ : Heap α
⊢ NoSibling nil

case h_2
α : Type u_1
le : α → α → Bool
x✝¹ x✝ : Heap α
a₂✝ : α
c₂✝ sibling✝ : Heap α
⊢ NoSibling (node a₂✝ c₂✝ nil)

case h_3
α : Type u_1
le : α → α → Bool
x✝¹ x✝ : Heap α
a₁✝ : α
c₁✝ sibling✝ : Heap α
⊢ NoSibling (node a₁✝ c₁✝ nil)

case h_4.inl
α : Type u_1
le : α → α → Bool
x✝¹ x✝ : Heap α
a₁✝ : α
c₁✝ sibling✝¹ : Heap α
a₂✝ : α
c₂✝ sibling✝ : Heap α
h✝ : le a₁✝ a₂✝ = true
⊢ NoSibling (node a₁✝ (node a₂✝ c₂✝ c₁✝) nil)

case h_4.inr
α : Type u_1
le : α → α → Bool
x✝¹ x✝ : Heap α
a₁✝ : α
c₁✝ sibling✝¹ : Heap α
a₂✝ : α
c₂✝ sibling✝ : Heap α
h✝ : ¬le a₁✝ a₂✝ = true
⊢ NoSibling (node a₂✝ (node a₁✝ c₁✝ c₂✝) nil)
α : Type u_1
le : α → α → Bool
s₁ s₂ : Heap α
⊢ NoSibling
    (match s₁, s₂ with
    | nil, nil => nil
    | nil, node a₂ c₂ sibling => node a₂ c₂ nil
    | node a₁ c₁ sibling, nil => node a₁ c₁ nil
    | node a₁ c₁ sibling, node a₂ c₂ sibling_1 =>
      if le a₁ a₂ = true then node a₁ (node a₂ c₂ c₁) nil else node a₂ (node a₁ c₁ c₂) nil)
split <;> try split
case h_4.inl
α : Type u_1
le : α → α → Bool
x✝¹ x✝ : Heap α
a₁✝ : α
c₁✝ sibling✝¹ : Heap α
a₂✝ : α
c₂✝ sibling✝ : Heap α
h✝ : le a₁✝ a₂✝ = true
⊢ NoSibling (node a₁✝ (node a₂✝ c₂✝ c₁✝) nil)

case h_4.inr
α : Type u_1
le : α → α → Bool
x✝¹ x✝ : Heap α
a₁✝ : α
c₁✝ sibling✝¹ : Heap α
a₂✝ : α
c₂✝ sibling✝ : Heap α
h✝ : ¬le a₁✝ a₂✝ = true
⊢ NoSibling (node a₂✝ (node a₁✝ c₁✝ c₂✝) nil)
case h_4
α : Type u_1
le : α → α → Bool
x✝¹ x✝ : Heap α
a₁✝ : α
c₁✝ sibling✝¹ : Heap α
a₂✝ : α
c₂✝ sibling✝ : Heap α
⊢ NoSibling (if le a₁✝ a₂✝ = true then node a₁✝ (node a₂✝ c₂✝ c₁✝) nil else node a₂✝ (node a₁✝ c₁✝ c₂✝) nil)
split