{α : Type} →
  (motive : Aesop.EMap (Lean.PHashSet Aesop.Match × Lean.PHashSet Aesop.Hyp) × Option α → Sort u_1) →
    (__discr : Aesop.EMap (Lean.PHashSet Aesop.Match × Lean.PHashSet Aesop.Hyp) × Option α) →
      ((map : Aesop.EMap (Lean.PHashSet Aesop.Match × Lean.PHashSet Aesop.Hyp)) → (a? : Option α) → motive (map, a?)) →
        motive __discr