sig
  type t = {
    lemma : Wp.Definitions.dlemma;
    depends : Wp.LogicUsage.logic_lemma list;
    mutable sequent : Wp.Conditions.sequent option;
  }
  val is_trivial : Wp.Wpo.VC_Lemma.t -> bool
  val cache_descr :
    Wp.Wpo.VC_Lemma.t -> (Wp.VCS.prover * Wp.VCS.result) list -> string
end