proposition: Lemma trans_succ : transitive succ.
proof: Proof. unfold succ. apply transp_trans. apply Rof_trans. intros t u v htu huv. apply rpo_trans with u; 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)