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