fact: Fixpoint subst_of_solved_eqns (l : solved_eqns) := match l with | (x, v) :: l' => extend (subst_of_solved_eqns l') x v | nil => id Sig end.
imports: Coq(Relations Wellfounded) CoLoR(ASubstitution ATerm EqUtil ListUtil LogicUtil VecUtil AVariables BoolUtil NatUtil SN AVariables Lexico)