proposition: Lemma bsucc_sub : rel_of_bool bsucc << succ.
proof: Proof. intros t u h. apply bsucc_sub. hyp. Qed.
imports: CoLoR(ATrs LogicUtil ARelation RelUtil SN ListUtil AMannaNess ACompat BoolUtil BoundNat) CoLoR(AMonAlg) CoLoR(AFilterBool VecUtil)