sig
  val lift : Term.constr Lazy.t
  val lift_proj_equivalence : Term.constr Lazy.t
  val lift_transitivity_left : Term.constr Lazy.t
  val lift_transitivity_right : Term.constr Lazy.t
  val lift_reflexivity : Term.constr Lazy.t
  val eval : Term.constr lazy_t
  val decide_thm : Term.constr lazy_t
  val lift_normalise_thm : Term.constr lazy_t
end