proposition: Lemma Rules_enum_Decr : of_list D' [=] Decr.
proof: Proof. unfold equiv. split; intro. apply enum_Decr_correct. hyp. apply enum_Decr_complete. hyp. Qed.
imports: CoLoR(ATrs AInterpretation BoolUtil LogicUtil EqUtil VecUtil SN RelUtil AWFMInterpretation NaryFunction NatUtil ARelation ARules SetUtil FunUtil VecMax AMorphism) Coq(List)