proposition: Lemma l_assoc : forall f t1 t2 t3, arity f = AC -> ac (Term f (Term f (t1 :: t2 :: nil) :: t3 :: nil)) (Term f (t1 :: (Term f (t2 :: t3 :: nil)) :: nil)).
proof: Proof. intros f t1 t2 t3 Af. unfold ac, th_eq. do 2 left. rewrite <- (empty_subst_is_id (Term f (Term f (t1 :: t2 :: nil) :: t3 :: nil))). rewrite <- (empty_subst_is_id (Term f (t1 :: Term f (t2 :: t3 :: nil) :: nil))). apply instance. left; apply a_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)