proposition: Lemma wf_succ : WF succ.
proof: Proof. apply wf_WF_transp. apply wf_inverse_image with (f:=term_of_aterm). apply wf_rpo. apply (prec_wf prec_nat). 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)