proposition: Lemma trans_succeq : transitive succeq.
proof: Proof. unfold succeq, Relation_Operators.union, transitive. intuition. left. apply trans_succ with y; hyp. left. revert H. unfold equiv_aterm, succ, transp, Rof. intro. rewrite <- equiv_rpo_equiv_2. apply H1. hyp. left. revert H1. unfold equiv_aterm, succ, transp, Rof. intro. rewrite equiv_rpo_equiv_1. apply H. hyp. right. apply trans_equiv_aterm with y; hyp. 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)