proposition: Lemma enum_Decr_complete : forall x, Decr x -> In x D'.
proof: Proof. intros. destruct H as [f [a [b [h]]]]. unfold enum_Decr. rewrite in_flat_map. exists f. split. apply Fs_ok. rewrite in_map_iff. exists (a,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)