fact: Fixpoint solved_eqns_wf (l : solved_eqns) := match l with | nil => True | (x, v) :: l' => mem x (vars v) = false /\ lforall (notin_solved_eqn x) l' /\ solved_eqns_wf l' /\ lforall (notin_vars_solved_eqn v) l' end.
imports: Coq(Relations Wellfounded) CoLoR(ASubstitution ATerm EqUtil ListUtil LogicUtil VecUtil AVariables BoolUtil NatUtil SN AVariables Lexico)