proposition: Lemma acc_inst_eq_subst : forall c sigma tau, (forall v, find X.eq_bool v sigma = find X.eq_bool v tau) -> forall v, find X.eq_bool v (acc_inst c sigma) = find X.eq_bool v (acc_inst c tau).
proof: Proof. intro c; induction c as [ | v c]; intros sigma tau H; simpl. trivial. intro x; refine (IHc _ _ _ _); clear x. intros x. assert (F := find_map_subst x v (apply_subst sigma (Var v)) sigma). assert (F' := find_map_subst x v (apply_subst tau (Var v)) tau). case_eq (find X.eq_bool x sigma); [intro x_val | idtac]; intro x_sigma; rewrite x_sigma in F; simpl in F; rewrite F; rewrite H in x_sigma; rewrite x_sigma in F'; simpl in F'; rewrite F'; trivial. rewrite H; trivial. Qed.
imports: Coq(Arith Wf_nat Wellfounded List Multiset Relations) CoLoR(closure decidable_set ordered_set more_list list_permut list_set list_sort dickson term_spec term)