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