proposition: Lemma is_sol_eqn_extend : forall s x (v : term) e, is_sol_eqn s (eqn_sub (single x v) e) <-> is_sol_eqn (extend s x (sub s v)) e.
proof: Proof. destruct e. unfold is_sol_eqn. simpl. rewrite !sub_sub, !sub_comp_single_extend. tauto. Qed.
imports: Coq(Relations Wellfounded) CoLoR(ASubstitution ATerm EqUtil ListUtil LogicUtil VecUtil AVariables BoolUtil NatUtil SN AVariables Lexico)