proposition: Lemma enum_correct : forall R a, In a (enum R) -> lab_rules (of_list R) a.
proof: Proof. intros. unfold enum in H. rewrite in_flat_map in H. do 2 destruct H. rewrite in_map_iff in H0. do 2 destruct H0. exists x0. exists (val_of_vec I x). intuition. Qed.
imports: CoLoR(ATrs AInterpretation BoolUtil LogicUtil EqUtil VecUtil SN RelUtil AWFMInterpretation NaryFunction NatUtil ARelation ARules SetUtil FunUtil VecMax AMorphism) Coq(List)