proposition: Lemma subst_of_solved_eqns_correct : forall l, solved_eqns_wf l -> is_sol_solved_eqns (subst_of_solved_eqns l) l.
proof: Proof. induction l; simpl. auto. set (s := subst_of_solved_eqns l). destruct a. unfold is_sol_solved_eqn. simpl. split_all. unfold extend at 1. simpl. rewrite (beq_refl beq_nat_ok), sub_extend_notin. sym. apply sub_eq_id'. intros. ded (lforall_notin_vars_solved_eqn_dom H2 H3). ded (dom_subst_of_solved_eqns H4). hyp. rewrite in_vars_mem, H. discr. apply is_sol_solved_eqns_extend; tauto. Qed.
imports: Coq(Relations Wellfounded) CoLoR(ASubstitution ATerm EqUtil ListUtil LogicUtil VecUtil AVariables BoolUtil NatUtil SN AVariables Lexico)