proposition: Lemma subst_aux : forall (sigma : substitution), (forall x u v, In (x,u) sigma -> In (x,v) sigma -> u = v) -> forall x u, In (x,u) sigma -> find X.eq_bool x sigma = Some u.
proof: Proof. intros sigma H x u xu_in_sig; case_eq (find X.eq_bool x sigma); [intros x_val x_sigma | intro x_sigma]. apply f_equal; apply (H x); trivial. destruct (find_mem _ _ X.eq_bool_ok _ _ x_sigma) as [x' [sig1 [sig2 [x_eq_x' H']]]]. subst x'; rewrite H'; apply in_or_app; right; left; apply eq_refl. apply False_rect; refine (find_not_found X.eq_bool _ x u sigma x_sigma (eq_var_bool_refl x) xu_in_sig). Qed.
imports: Coq(List Relations Wellfounded Arith Setoid) CoLoR(closure more_list weaved_relation dickson term_spec equational_theory_spec)