proposition: Lemma no_var_in_term_inv : forall x x_val y_val z, var_in_term z x_val = false -> var_in_term z y_val = false -> var_in_term z (apply_subst ((x,x_val) :: nil) y_val) = false.
proof: Proof. intros x x_val w_val' z z_not_in_x_val z_not_in_w_val'; assert (var_in_term z (apply_subst ((x, x_val) :: nil) w_val') <> true). intro H1; rewrite var_in_term_is_sound in H1. destruct (var_in_subterm2 _ _ (in_impl_mem (@eq _) (fun a => eq_refl _) _ _ H1)) as [p H''']. assert (H4 := subterm_in_instantiated_term _ _ _ H'''). case_eq (subterm_at_pos w_val' p); [intros [u | f l] | idtac]; intro Hsub; rewrite Hsub in H4. simpl in H4; revert H4; generalize (X.eq_bool_ok u x); case (X.eq_bool u x); [intro u_eq_x | intro u_diff_x]. intro H4; subst u x_val; assert (z_in_x_val' : var_in_term z (Var z) = true). simpl; generalize (X.eq_bool_ok z z); case (X.eq_bool z z); [intros _; trivial | intro z_diff_z; apply False_rect; apply z_diff_z; trivial]. rewrite z_in_x_val' in z_not_in_x_val; discriminate. intro H4; injection H4; clear H4; intro H4; subst u. assert (z_in_w_val' := var_in_subterm z _ _ Hsub (or_introl _ (eq_refl _))). rewrite <- var_in_term_is_sound in z_in_w_val'. rewrite z_not_in_w_val' in z_in_w_val'; discriminate. discriminate. destruct H4 as [u [q [q' [H4 [H5 [H6 H7]]]]]]. simpl in H7; revert H7; generalize (X.eq_bool_ok u x); case (X.eq_bool u x); [intro u_eq_x | intro u_diff_x]. intro H7; subst u; assert (z_in_x_val := var_in_subterm z _ _ H7 (or_introl _ (eq_refl _))). rewrite <- var_in_term_is_sound in z_in_x_val. rewrite z_not_in_x_val in z_in_x_val; discriminate. intro H7; destruct q'; [injection H7; clear H7; intro H7; subst u | discriminate]. rewrite <- app_nil_end in H4; subst q. rewrite Hsub in H6; discriminate. destruct (var_in_term z (apply_subst ((x, x_val) :: nil) w_val')); [absurd (true = true) | idtac]; 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)