sig
  type sigma
  val sigma :
    Wp.Lang.F.var list -> Wp.Lang.F.term list -> Wp.Lang.Subst.sigma
  val e_apply : Wp.Lang.Subst.sigma -> Wp.Lang.F.term -> Wp.Lang.F.term
  val p_apply : Wp.Lang.Subst.sigma -> Wp.Lang.F.pred -> Wp.Lang.F.pred
end