sig
  type t = Proof.step
  val kind : Proof.Step.t -> Proof.kind
  val parents : Proof.Step.t -> Proof.parent list
  val infos : Proof.Step.t -> Proof.infos
  val compare : Proof.Step.t -> Proof.Step.t -> int
  val hash : Proof.Step.t -> int
  val equal : Proof.Step.t -> Proof.Step.t -> bool
  val trivial : Proof.Step.t
  val by_def : Logtk.ID.t -> Proof.Step.t
  val data :
    Proof.statement_src -> Logtk.Type.t Logtk.Statement.data -> Proof.Step.t
  val assert_ : Proof.statement_src -> Proof.Step.t
  val goal : Proof.statement_src -> Proof.Step.t
  val lemma : Proof.Step.t
  val assert' :
    ?loc:Loc.t -> file:string -> name:string -> unit -> Proof.Step.t
  val goal' :
    ?loc:Loc.t -> file:string -> name:string -> unit -> Proof.Step.t
  val inference :
    ?infos:Proof.infos ->
    ?check:Proof.check ->
    rule:Proof.rule -> Proof.parent list -> Proof.Step.t
  val simp :
    ?infos:Proof.infos ->
    ?check:Proof.check ->
    rule:Proof.rule -> Proof.parent list -> Proof.Step.t
  val esa :
    ?infos:Proof.infos ->
    ?check:Proof.check ->
    rule:Proof.rule -> Proof.parent list -> Proof.Step.t
  val is_trivial : Proof.Step.t -> bool
  val is_by_def : Proof.Step.t -> bool
  val is_assert : Proof.Step.t -> bool
  val is_goal : Proof.Step.t -> bool
  val rule : Proof.Step.t -> Proof.rule option
  val distance_to_goal : Proof.Step.t -> int option
  val pp : Proof.Step.t CCFormat.printer
end