proposition: Lemma ac_const : forall c t, ac (Term c nil) t -> t = Term c nil.
proof: Proof. intros c [ v | f [ | t l]] H; generalize (ac_top_eq H). contradiction. intros; subst; trivial. intros _; assert (S := ac_size_eq H); simpl in S; injection S; clear S; intro S; absurd (1 <= 0). auto with arith. pattern 0 at 2; rewrite S; apply Nat.le_trans with (size t). apply size_ge_one. auto with arith. Qed.
imports: Coq(Arith List Relations) CoLoR(closure more_list weaved_relation list_sort term_spec equational_theory ac cf_eq_ac rpo)