let lazy_sigma a f l =
  assert(not(is_var a) && Sym.eq (Term.App.sym_of a) f);
  let m = Term.App.args_of a in
  if try List.for_all2 eq l m with Invalid_argument _ -> false then
    a
  else 
    sigma f l