fact: Fixpoint lab v t := match t with | Var x => Var x | Fun f ts => Fun' (mk (pi f (Vmap (int v) ts))) (Vmap (lab v) ts) end.
imports: CoLoR(ATrs AInterpretation BoolUtil LogicUtil EqUtil VecUtil SN RelUtil AWFMInterpretation NaryFunction NatUtil ARelation ARules SetUtil FunUtil VecMax AMorphism) Coq(List)