proposition: Lemma ren_caps_eq : forall n (ts : terms n) k, Vmap_sum (Vmap capa ts) (fresh k (sum (Vmap capa ts))) = ren_caps k ts.
proof: Proof. induction ts; simpl; intros. refl. rewrite Vbreak_fresh. apply Vcons_eq_intro. refl. rewrite IHts. refl. Qed.
imports: CoLoR(LogicUtil ACalls ATrs VecUtil ListUtil NatUtil RelUtil)