proposition: Lemma well_formed_cf_build : forall f l, arity f = AC -> 1 <= length l -> (forall t, In t l -> well_formed_cf t) -> (forall t, In t l -> match t with | Var _ => True | Term g _ => f <> g end) -> well_formed_cf (build f l).
proof: Proof. intros f l Af Ll Wl Al; destruct l as [ | t1 [ | t2 l]]. simpl in Ll; absurd (1 <= 0); trivial; auto with arith. apply Wl; left; trivial. rewrite build_eq_Term; [idtac | simpl; auto with arith]. apply well_formed_cf_fold; split. intros u In_u; rewrite <- in_quick_in in In_u. apply Wl; trivial. rewrite Af; split; [idtac | split]. rewrite length_quicksort; simpl; auto with arith. apply quick_sorted. intros u In_u; rewrite <- in_quick_in in In_u. apply Al; trivial. Qed.
imports: Coq(Relations List Arith Morphisms) CoLoR(more_list list_permut list_sort term_spec term_o equational_theory_spec equational_theory)