proposition: Lemma enum_complete : forall R a, lab_rules (of_list R) a -> In a (enum R).
proof: Proof. intros. do 3 destruct H. set (n := maxvar_rules R). unfold enum. rewrite in_flat_map. exists (vec_of_val x0 (S n)). split. apply enum_tuple_complete. subst. change (In (lab_rule x0 x) (map (lab_rule (fval x0 (S n))) R)). rewrite map_lab_rule_fval. apply in_map. hyp. unfold n. lia. Qed.
imports: CoLoR(ATrs AInterpretation BoolUtil LogicUtil EqUtil VecUtil SN RelUtil AWFMInterpretation NaryFunction NatUtil ARelation ARules SetUtil FunUtil VecMax AMorphism) Coq(List)