let nparamod metasenv subst context t =
  let module C = struct
    let metasenv = metasenv
    let subst = subst
    let context = context
  end
  in
  let module B = NCicBlob.NCicBlob(C) in
  let module Pp = Pp.Pp (B) in
  let res,vars = B.embed t in
  let module FU = Founif.Founif(B) in
  let test_unification vars = function
    | Terms.Node [_; _; lhs; rhs] ->
	prerr_endline "Unification test :";
	prerr_endline (Pp.pp_foterm lhs);
	prerr_endline (Pp.pp_foterm rhs);
	FU.unification vars [] lhs rhs
    | _ -> assert false
  in
  let subst,vars = test_unification vars res in
    prerr_endline "Result :";
    prerr_endline (Pp.pp_foterm res);
    prerr_endline "Substitution :";
    prerr_endline (Pp.pp_substitution subst)
;;