proposition: Lemma is_sol_solved_eqns_extend : forall s n v l, lforall (notin_solved_eqn n) l -> is_sol_solved_eqns s l -> is_sol_solved_eqns (extend s n v) l.
proof: Proof. induction l; simpl. auto. destruct a. unfold notin_solved_eqn at 1, is_sol_solved_eqn. simpl. split_all. unfold extend at 1. case_beq_nat n0 n. tauto. rewrite H0. sym. apply sub_extend_notin. rewrite in_vars_mem, H3. discr. Qed.
imports: Coq(Relations Wellfounded) CoLoR(ASubstitution ATerm EqUtil ListUtil LogicUtil VecUtil AVariables BoolUtil NatUtil SN AVariables Lexico)