proposition: Lemma trans_succ : transitive succ.
proof: Proof. apply filter_trans. apply trans_succ. Qed.
imports: CoLoR(ATrs LogicUtil ARelation RelUtil SN ListUtil AMannaNess ACompat BoolUtil BoundNat) CoLoR(AMonAlg) CoLoR(AFilterBool VecUtil)