proposition: Lemma tail_total_ordering : forall sigma v v_val c, list_exists (fun z : variable => var_in_term z v_val) c = false -> is_a_total_oc_ordering sigma c = true -> is_a_total_oc_ordering (map_subst (fun (_ : variable) (t : term) => apply_subst ((v, v_val) :: nil) t) sigma) c = true.
proof: Proof. intros sigma v v_val l; induction l as [ | z l]; simpl; intros H' Hoc; trivial. assert (F := find_map_subst z v v_val sigma). case_eq (find X.eq_bool z sigma); [intro z_val | idtac]; intro z_sigma; rewrite z_sigma in F; rewrite z_sigma in Hoc; rewrite F. case_eq (var_in_term z v_val); intro z_in_v_val; rewrite z_in_v_val in H'. discriminate. case_eq (var_in_term z z_val); intro z_in_z_val; rewrite z_in_z_val in Hoc. discriminate. simpl in H'; simpl in Hoc. rewrite (no_var_in_term_inv v v_val z_val z z_in_v_val z_in_z_val). simpl. case_eq (list_exists (fun z : variable => var_in_term z z_val) l); intro Hoc'; rewrite Hoc' in Hoc; [discriminate | simpl in Hoc]. assert (Hoc'' := list_exists_is_complete_false _ _ Hoc'). case_eq (list_exists (fun z0 : variable => var_in_term z0 (apply_subst ((v, v_val) :: nil) z_val)) l); intro Goc. rewrite list_exists_is_sound in Goc. destruct Goc as [w [w_in_l Goc']]. rewrite <- Goc'; symmetry. apply no_var_in_term_inv. apply (list_exists_is_complete_false _ _ H' w w_in_l). apply (Hoc'' w w_in_l). apply IHl; trivial. revert Hoc; 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]. 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)