proposition: Lemma succ_succeq_compat : absorbs_left succ succeq.
proof: Proof. intros t v [u [[h1|h1] h2]]. apply rpo_trans with (term_of_aterm u); hyp. unfold succ, transp, Rof. rewrite equiv_rpo_equiv_1. apply h2. 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)