proposition: Lemma build_eq_Term : forall f l, 2 <= length l -> build f l = Term f (quicksort l).
proof: Proof. intros f l Ll; destruct l as [ | u [ | v l]]; simpl; trivial. simpl in Ll; absurd (2 <= 1); auto with arith. Qed.
imports: Coq(Relations List Arith Morphisms) CoLoR(more_list list_permut list_sort term_spec term_o equational_theory_spec equational_theory)