proposition: Lemma Vmap_sum_conc_forall : forall n (ts : terms n), (Vforall (fun t => fcap_aliens (capa t) = t) ts) -> Vmap_sum (Vmap capa ts) (conc (Vmap capa ts)) = ts.
proof: Proof. induction ts; simpl; intros. refl. destruct H. rewrite Vbreak_app. unfold fcap_aliens in H. rewrite H. apply Vtail_eq. apply IHts. hyp. Qed.
imports: Coq(Sumbool) CoLoR(LogicUtil ACalls ATrs VecUtil ListUtil NatUtil EqUtil)