proposition: Lemma comm : forall f t1 t2, arity f = C \/ arity f = AC -> ac (Term f (t1 :: t2 :: nil)) (Term f (t2 :: t1 :: nil)).
proof: Proof. intros f t1 t2 Af. unfold ac, th_eq. do 2 left. rewrite <- (empty_subst_is_id (Term f (t1 :: t2 :: nil))). rewrite <- (empty_subst_is_id (Term f (t2 :: t1 :: nil))). apply instance. left; apply c_axiom; trivial. Qed.
imports: Coq(Relations List Arith Morphisms) CoLoR(more_list list_permut list_sort term_spec term_o equational_theory_spec equational_theory)