proposition: Lemma idem_sol : forall sigma, (forall x y, VSet.mem x (domain_of_subst sigma) -> VSet.mem y (domain_of_subst sigma) -> var_in_term x (apply_subst sigma (Var y)) = false) -> is_a_solution (mk_pb sigma nil) sigma.
proof: Proof. intros sigma Idem; split. intros; contradiction. simpl; intros x. case_eq (find X.eq_bool x sigma); [intro x_val | idtac]; intro x_sigma; trivial. symmetry; apply apply_subst_outside_dom. intro y; split; [idtac | intro; contradiction]. intro H. assert (H1 := VSet.inter_1 _ _ _ H). assert (H2 := VSet.inter_2 _ _ _ H). clear H. assert (H3 : VSet.mem x (domain_of_subst sigma)). rewrite var_in_domain_of_subst; rewrite x_sigma; discriminate. assert (Hi := Idem y x H1 H3). assert (H2' : In y (var_list x_val)). revert H2; pattern x_val; apply term_rec3; [intro v | intros f l]. unfold VSet.mem, VSet.singleton, DecVar.eq_A; simpl. intros [H | H]; [subst; left; reflexivity | contradiction]. induction l as [ | t l]. unfold VSet.mem, VSet.singleton, DecVar.eq_A; simpl. intros; contradiction. intros IH y_in_tl. unfold set_of_variables in y_in_tl. destruct (VSet.union_12 _ _ _ y_in_tl) as [y_in_t | y_in_l]. simpl; apply in_or_app; left. apply (IH t (or_introl _ (eq_refl _)) y_in_t). simpl; apply in_or_app; right. refine (IHl _ y_in_l). intros; apply IH. right; trivial. trivial. rewrite <- var_in_term_is_sound in H2'; simpl in Hi; rewrite x_sigma in Hi; rewrite Hi in H2'; discriminate. 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)