fact: Fixpoint ren_caps k n (ts : terms n) : terms n := match ts in vector _ n return terms n with | Vnil => Vnil | Vcons t ts => Vcons (ren_cap k t) (ren_caps (k + nb_aliens t) ts) end.
imports: CoLoR(LogicUtil ACalls ATrs VecUtil ListUtil NatUtil RelUtil)