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