proposition: Lemma subst_of_solved_eqns_most_general : forall s l, solved_eqns_wf l -> is_sol_solved_eqns s l -> forall x, s x = sub (theta l s) (subst_of_solved_eqns l x).
proof: Proof. induction l. refl. destruct a. unfold is_sol_solved_eqns. simpl. unfold is_sol_solved_eqn at 1. simpl. split_all. unfold extend. case_beq_nat x n. rewrite H0. apply sub_eq'. intros. unfold theta. simpl. mem. case_beq_nat x x0; simpl. rewrite H in H5. discr. case_eq (mem x0 (dom l)); intro H8. ded (lforall_notin_vars_solved_eqn_mem H4 H8). rewrite H5 in H7. discr. refl. rewrite IHl; try tauto. apply sub_eq'. intros. unfold theta. simpl. mem. case_beq_nat n x0. simpl. ded (lforall_notin_solved_eqn_mem H2 H5). rewrite H7 in H6. discr. simpl. refl. Qed.
imports: Coq(Relations Wellfounded) CoLoR(ASubstitution ATerm EqUtil ListUtil LogicUtil VecUtil AVariables BoolUtil NatUtil SN AVariables Lexico)