proposition: Lemma apply_subst_outside_dom : forall sigma t, VSet.eq_set (VSet.inter (domain_of_subst sigma) (set_of_variables t)) VSet.empty -> apply_subst sigma t = t.
proof: Proof. intros sigma t; pattern t; apply term_rec3; clear t. intros v; induction sigma as [ | [x t] sigma]; trivial. intro; simpl. generalize (X.eq_bool_ok v x); case (X.eq_bool v x); [intro v_eq_x | intro v_diff_x]. subst v; assert (H' : VSet.mem x VSet.empty). rewrite <- (H x); apply VSet.inter_12; [ simpl; apply VSet.add_1 | left; reflexivity]. contradiction. apply IHsigma; intro z; split; [intro z_in_x_dom_sig | intro z_in_empty]. rewrite <- (H z); apply VSet.inter_12. simpl; apply VSet.add_2; apply (VSet.inter_1 _ _ _ z_in_x_dom_sig). apply (VSet.inter_2 _ _ _ z_in_x_dom_sig). contradiction. intros f l IH H; simpl; simpl in H; apply (f_equal (fun l => Term f l)); induction l as [ | s l]. trivial. simpl; rewrite (IH s); [rewrite IHl; trivial | left; trivial | idtac ]. intros; apply IH; trivial; right; trivial. intro z; split; [intro z_in_dom_sig_l | intro z_in_empty]. rewrite <- (H z); apply VSet.inter_12. simpl; apply (VSet.inter_1 _ _ _ z_in_dom_sig_l). apply VSet.union_2; apply (VSet.inter_2 _ _ _ z_in_dom_sig_l). contradiction. intro z; split; [intro z_in_dom_sig_s | intro z_in_empty]. rewrite <- (H z); apply VSet.inter_12. simpl; apply (VSet.inter_1 _ _ _ z_in_dom_sig_s). apply VSet.union_1; apply (VSet.inter_2 _ _ _ z_in_dom_sig_s). contradiction. 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)