Comment by krapht

Any chance this could be implemented for automated proof synthesis? Would love to see this used in F* or Lean.