proposition: Lemma bsucc_sub : rel_of_bool bsucc << succ.
proof: Proof. intros t u. unfold rel. intro h. apply bsucc_ok. 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)