{α : Type} →
  Aesop.InstMap →
    Aesop.SlotIndex →
      Lean.Expr →
        (Lean.PHashSet Aesop.Match →
            Lean.PHashSet Aesop.Hyp → Lean.PHashSet Aesop.Match × Lean.PHashSet Aesop.Hyp × α) →
          Lean.MetaM (Aesop.InstMap × α)