sig
val lift : Coq.lazy_ref
val lift_proj_equivalence : Coq.lazy_ref
val lift_transitivity_left : Coq.lazy_ref
val lift_transitivity_right : Coq.lazy_ref
val lift_reflexivity : Coq.lazy_ref
val eval : Coq.lazy_ref
val decide_thm : Coq.lazy_ref
val lift_normalise_thm : Coq.lazy_ref
end