subst is now in three parts:
- first it collects one equality per lsymbol that was given
- it generates a list of tdecl which corresponds to the task minus
  the lsymbols and equalities collected before. It also substitutes all
  decls with these appropriate lsymbol erased.
- it tries to add all this new tdecl into a new task with the safe
  Task.add_tdecl function. It tries to keep the order of decl as much as
  possible.

There is room for improvement (in particular on efficiency of
substitution).