diff --git a/src/core/term.ml b/src/core/term.ml
index d3a60899cdfe91eb0e2b89d15055a1ab6de4c2fe..cd0b0c294db457fcc40bd084053e234179c80e88 100644
--- a/src/core/term.ml
+++ b/src/core/term.ml
@@ -1896,3 +1896,33 @@ let f_map_simp fnT fnF f = f_label_copy f (match f.f_node with
 
 let f_map_simp fnT = f_map_simp (protect fnT)
 
+(** Proposition of another fold *)
+(* Type in terms and formulae *)
+let rec t_fold_ty fty s t =
+  let s = t_fold_unsafe (t_fold_ty fty) (f_fold_ty fty) s t in
+  let s = fty s t.t_ty in
+  match t.t_node with
+    | Teps fb ->
+      let vs,_,_ = fb in
+      fty s vs.vs_ty
+    | _ -> s
+
+and f_fold_ty fty s f =
+  let s = f_fold_unsafe (t_fold_ty fty) (f_fold_ty fty) s f in
+  match f.f_node with
+    | Fquant (_,fq) ->
+      let (vsl,_,_,_) = fq in
+      List.fold_left (fun s vs -> fty s vs.vs_ty) s vsl
+    | _ -> s
+
+let rec t_fold_sig fty s t =
+  let s = t_fold_unsafe (t_fold_sig fty) (f_fold_sig fty) s t in
+  match t.t_node with
+    | Tapp (fs,tl) -> fty s fs (List.map (fun t -> t.t_ty) tl)
+    | _ -> s
+
+and f_fold_sig fty s f =
+  let s = f_fold_unsafe (t_fold_sig fty) (f_fold_sig fty) s f in
+  match f.f_node with
+    | Fapp (fs,tl) -> fty s fs (List.map (fun t -> t.t_ty) tl)
+    | _ -> s
diff --git a/src/core/term.mli b/src/core/term.mli
index c226921ba4b465230798fb7cd9d868ab764c1216..e070659bc23447ffd780dee0c7ecc149da3f8b83 100644
--- a/src/core/term.mli
+++ b/src/core/term.mli
@@ -506,3 +506,9 @@ exception NoMatch
 val t_match : term Mvs.t -> term -> term -> term Mvs.t
 val f_match : term Mvs.t -> fmla -> fmla -> term Mvs.t
 
+(** Proposition of another fold *)
+val t_fold_ty : ('a -> ty -> 'a) -> 'a -> term -> 'a
+val f_fold_ty : ('a -> ty -> 'a) -> 'a -> fmla -> 'a
+
+val t_fold_sig : ('a -> lsymbol -> ty list -> 'a) -> 'a -> term -> 'a
+val f_fold_sig : ('a -> lsymbol -> ty list -> 'a) -> 'a -> fmla -> 'a