let sigma f al = 
  assert(Sym.Pprod.is Sig.f);
  match al with
    | [a; b] -> mk_mult a b
    | _ -> Term.App.mk_app Sym.Pprod.mk_mult al