let matching2  (f,t) =
  let rec 
    match_rec s = function  
        (Var(x), t) -> add_subst1 s (x,t)
      | ( Operation(op_f,sons_f),Operation(op_t,sons_t)) ->
          if op_f = op_t then 
            try 
              (List.fold_left match_rec s
                 (List.combine sons_f sons_t))
            with _ -> raise Match_exc1
          else raise Match_exc1
      | _ -> raise Match_exc1
  in
    match_rec [] (f,t)