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