proposition: Lemma Vmap_sum_conc : forall n (ts : terms n), Vmap_sum (Vmap capa ts) (conc (Vmap capa ts)) = ts.
proof: Proof. intros. apply Vmap_sum_conc_forall. apply Vforall_intro. intros. apply sub_capa. Qed.
imports: Coq(Sumbool) CoLoR(LogicUtil ACalls ATrs VecUtil ListUtil NatUtil EqUtil)