type ident = string

let nouveau_symbole
   : ident -> ident  = 

  let f = ref (fun _ -> 0) in fun ident -> begin
    let i = !f ident in
    let g = !f in
    f := (fun k -> if k = ident then i + 1 else g k);
    ident ^ "__" ^ string_of_int i
  end

type 'a resultat = {
  res_axiomes : (ident * 'a) list;
  res_theoremes : (ident * 'a) list;
}

let rec plier_gauche f a = function 
  | 0 -> a
  | k -> plier_gauche f (f a k) (k - 1)  

let iterer f = plier_gauche (fun accu k -> (f k)::accu) []