proposition: Lemma enum_Decr_empty : enum_Decr beq_ok Fs L2s = nil.
proof: Proof. unfold enum_Decr. unfold L2s. simpl. induction Fs. refl. simpl. hyp. Qed.
imports: CoLoR(ATrs AInterpretation BoolUtil LogicUtil EqUtil VecUtil SN RelUtil AWFMInterpretation NaryFunction NatUtil ARelation ARules SetUtil FunUtil VecMax AMorphism) Coq(List)