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