sig
  val check_tau : Lang.tau -> bool
  val check_term : Lang.F.term -> bool
  class type engine =
    object
      method callstyle : Qed.Engine.callstyle
      method pp_atom : Format.formatter -> Lang.F.term -> unit
      method pp_flow : Format.formatter -> Lang.F.term -> unit
    end
  val f_nil : Lang.Fun.t
  val f_elt : Lang.Fun.t
  val f_nth : Lang.Fun.t
  val f_cons : Lang.Fun.t
  val f_concat : Lang.Fun.t
  val f_repeat : Lang.Fun.t
  val export : #Vlist.engine -> Format.formatter -> Lang.F.term list -> unit
  val pretty : #Vlist.engine -> Format.formatter -> Lang.F.term list -> unit
  val elements :
    #Vlist.engine -> Format.formatter -> Lang.F.term list -> unit
  val pprepeat :
    #Vlist.engine -> Format.formatter -> Lang.F.term list -> unit
  val shareable : Lang.F.term -> bool
end