proposition: Lemma bsucc_sub : rel_of_bool bsucc << succ.
proof: Proof. intros t u. unfold rel_of_bool, bsucc, bool_of_rel. case (succ'_dec t u); intros. apply succ'_sub. hyp. discr. Qed.
imports: CoLoR(ATrs LogicUtil ARelation RelUtil SN ListUtil AMannaNess ACompat BoolUtil BoundNat) CoLoR(AMonAlg)