fact: Fixpoint dom (l : solved_eqns) := match l with | (x, _) :: l' => add x (dom l') | nil => empty end.
imports: Coq(Relations Wellfounded) CoLoR(ASubstitution ATerm EqUtil ListUtil LogicUtil VecUtil AVariables BoolUtil NatUtil SN AVariables Lexico)