{P : Sort u} →
  {e' proof : Lean.Expr} →
    {done : optParam Bool false} →
      {e'' proof' : Lean.Expr} →
        {done' : optParam Bool false} →
          Lean.Meta.Sym.Simp.Result.step e' proof done = Lean.Meta.Sym.Simp.Result.step e'' proof' done' →
            (e' = e'' → proof = proof' → done = done' → P) → P