@type t() :: %Theoria.Simp.Step{
  after: Theoria.Term.t(),
  before: Theoria.Term.t(),
  path: [atom()],
  proof: Theoria.Term.t() | nil,
  proof_status:
    :checked
    | :not_requested
    | :missing_rule_proof
    | :unsupported_path
    | :kernel_rejected
    | nil,
  rule: atom(),
  source: atom()
}