proposition: Lemma is_sol_eqns_extend : forall s x (v : term) l, is_sol_eqns s (map (eqn_sub (single x v)) l) <-> is_sol_eqns (extend s x (sub s v)) l.
proof: Proof. induction l; simpl; split_all; try tauto; revert H; unfold is_sol_eqn; simpl; rewrite !sub_sub, !sub_comp_single_extend; auto. Qed.
imports: Coq(Relations Wellfounded) CoLoR(ASubstitution ATerm EqUtil ListUtil LogicUtil VecUtil AVariables BoolUtil NatUtil SN AVariables Lexico)