proposition: Lemma enum_tuple_complete : forall n (ds : vector I n), In ds (enum_tuple n).
proof: Proof. induction n; simpl; intros. VOtac. auto. rewrite in_flat_map. exists (Vtail ds). split. apply IHn. set (f := fun d : I => Vcons d (Vtail ds)). VSntac ds. change (In (f (Vhead ds)) (map f Is)). apply in_map. apply Is_ok. Qed.
imports: CoLoR(ATrs AInterpretation BoolUtil LogicUtil EqUtil VecUtil SN RelUtil AWFMInterpretation NaryFunction NatUtil ARelation ARules SetUtil FunUtil VecMax AMorphism) Coq(List)