proposition: Lemma trans_equiv_aterm : transitive equiv_aterm.
proof: Proof. unfold equiv_aterm. apply Rof_trans. apply (@RelationClasses.Equivalence_Transitive _ _ (equiv_equiv Prec)). Qed.
imports: CoLoR(LogicUtil ATerm VecUtil) CoLoR(term_spec EqUtil) CoLoR(NatUtil) Coq(List Relations) CoLoR(term SN ASubstitution) CoLoR(rpo rpo_extension) CoLoR(ARedPair ARelation RelUtil BoolUtil)