proposition: Lemma subst_eq_vars : forall t sigma sigma', (forall v, In v (var_list t) -> apply_subst sigma (Var v) = apply_subst sigma' (Var v)) <-> apply_subst sigma t = apply_subst sigma' t.
proof: Proof. intros t sigma sigma'; split. pattern t; apply term_rec3; clear t. intros v H; apply H; left; trivial. intros f l IHl H. simpl; apply (f_equal (fun l => Term f l)). apply map_eq; intros t t_in_l; apply IHl; trivial. intros v v_in_t; apply H. destruct (In_split _ _ t_in_l) as [l1 [l2 H']]; subst. apply var_in_subterm with t (length l1 :: nil); trivial. simpl; rewrite nth_error_at_pos; trivial. pattern t; apply term_rec3; clear t. intros v H; simpl; intros x [x_eq_v | F]; [subst; trivial | contradiction]. intros f l IHl H; simpl in H; injection H; clear H; intro H. intros v v_in_l; rewrite var_list_unfold in v_in_l; induction l as [ | t l]. contradiction. simpl in H; injection H; clear H; intros H H'. simpl in v_in_l. destruct (in_app_or _ _ _ v_in_l) as [v_in_t | v_in_l']. apply IHl with t; trivial. left; trivial. apply IHl0; trivial. intros s s_in_l H'' x x_in_s; apply (IHl s); trivial. right; trivial. Qed.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set term_spec) CoLoR.Util.Nat(NatCompat)