sig
  val decl_map :
    (Why3.Term.term -> Why3.Term.term) ->
    (Why3.Term.term -> Why3.Term.term) -> Decl.decl -> Decl.decl
  val decl_fold :
    ('a -> Why3.Term.term -> 'a) ->
    ('a -> Why3.Term.term -> 'a) -> 'a -> Decl.decl -> 'a
  val decl_map_fold :
    ('a -> Why3.Term.term -> 'a * Why3.Term.term) ->
    ('a -> Why3.Term.term -> 'a * Why3.Term.term) ->
    'a -> Decl.decl -> 'a * Decl.decl
end