sig
  val of_exp :
    Qed.Engine.cmode ->
    Lang.F.term -> (Lang.F.var, Lang.F.Fun.t) Qed.Engine.ftrigger
  val of_term : Lang.F.term -> (Lang.F.var, Lang.F.Fun.t) Qed.Engine.ftrigger
  val of_pred : Lang.F.pred -> (Lang.F.var, Lang.F.Fun.t) Qed.Engine.ftrigger
  val collect :
    Lang.F.Vars.t ->
    (Lang.F.Vars.elt, 'a) Qed.Engine.ftrigger -> Lang.F.Vars.t
  val vars :
    (Lang.F.Vars.elt, Lang.lfun) Qed.Engine.ftrigger -> Lang.F.Vars.t
  val binders : Lang.F.term -> Lang.F.var list * Lang.F.term
  val plug :
    (Lang.F.Vars.elt, 'a) Qed.Engine.ftrigger list list ->
    Lang.F.pred -> Lang.F.Vars.elt list * Lang.F.pred
end