proposition: Lemma is_sol_solved_eqns_sub : forall s s' l, is_sol_solved_eqns s l -> is_sol_solved_eqns (sub_comp s' s) l.
proof: Proof. induction l; simpl; split_all. destruct a. revert H. unfold is_sol_solved_eqn. simpl. intro. rewrite <- sub_sub, <- H. refl. Qed.
imports: Coq(Relations Wellfounded) CoLoR(ASubstitution ATerm EqUtil ListUtil LogicUtil VecUtil AVariables BoolUtil NatUtil SN AVariables Lexico)