fact: Definition is_well_formed_sol pb sigma := (exists sigma', is_rough_sol pb sigma' /\ (forall v, In v (existential_vars pb) \/ apply_cf_subst sigma (Var v) = apply_cf_subst sigma' (Var v)) /\ (well_formed_cf_subst sigma')).
imports: Coq(Arith List) CoLoR(more_list list_sort term_spec ac cf_eq_ac)