sig
  type t = Proof.parent
  val from : Proof.proof -> Proof.Parent.t
  val from_subst :
    Proof.proof Logtk.Scoped.t -> Logtk.Subst.t -> Proof.Parent.t
  val proof : Proof.Parent.t -> Proof.proof
end