let update c s =
  let update1 (a, i, rho) = 
    if i = Sign.F then
      raise Exc.Inconsistent
    else 
      begin
        Trace.msg "c" "Update" (a, i) (Pretty.infix Term.pp " in " Sign.pp);
        changed := Term.Set.add a !changed;
        Term.Map.add a (i, rho) s
      end 
  in
  let (a, i, rho) = Fact.d_cnstrnt c in
    try
      let (j, sigma) = apply s a in
        if Sign.sub j i then 
          s 
        else 
          update1 (a, Sign.inter i j, Fact.mk_rule "Conj" [rho; sigma])
    with
        Not_found -> 
          update1 (a, i, rho)