proposition: Lemma enum_Decr_correct : forall x, In x D' -> Decr x.
proof: Proof. intros. unfold enum_Decr in H. rewrite in_flat_map in H. destruct H as [f]. destruct H. rewrite in_map_iff in H0. destruct H0 as [[a b]]. destruct H0. exists f. exists a. exists b. rewrite L2s_ok. auto. Qed.
imports: CoLoR(ATrs AInterpretation BoolUtil LogicUtil EqUtil VecUtil SN RelUtil AWFMInterpretation NaryFunction NatUtil ARelation ARules SetUtil FunUtil VecMax AMorphism) Coq(List)