∀ {α : Type u_1} (motive : Option (Batteries.PairingHeapImp.Heap α) → Prop)
  (x : Option (Batteries.PairingHeapImp.Heap α)),
  (x = none → motive none) → (∀ (tl : Batteries.PairingHeapImp.Heap α), x = some tl → motive (some tl)) → motive x