fact: Parameter add_new_var_to_rough_sol : forall pb sigma t, well_formed_pb pb -> is_rough_sol pb sigma -> (is_rough_sol pb ((fresh_var pb, t) :: sigma)).
imports: Coq(Arith List) CoLoR(more_list list_sort term_spec ac cf_eq_ac)