fact: Fixpoint Vmap_sum n (cs : Caps n) : terms (sum cs) -> terms n := match cs as cs in vector _ n return terms (sum cs) -> terms n with | Vnil => fun _ => Vnil | Vcons c cs' => fun ts => let (hd,tl) := Vbreak ts in Vcons (fcap c hd) (Vmap_sum cs' tl) end.
imports: CoLoR(LogicUtil ACalls ATrs VecUtil ListUtil NatUtil RelUtil)