fact: Definition is_sol s p := match p with | None => False | Some (l1, l2) => is_sol_solved_eqns s l1 /\ is_sol_eqns s l2 end.
imports: Coq(Relations Wellfounded) CoLoR(ASubstitution ATerm EqUtil ListUtil LogicUtil VecUtil AVariables BoolUtil NatUtil SN AVariables Lexico)