proposition: Lemma ren_caps_cast : forall n1 (ts : terms n1) n2 (e : n1=n2) k, ren_caps k (Vcast ts e) = Vcast (ren_caps k ts) e.
proof: Proof. induction ts; intros; destruct n2; try discr. rewrite !Vcast_refl. refl. simpl. rewrite !Vcast_cons. simpl. rewrite IHts. refl. Qed.
imports: CoLoR(LogicUtil ACalls ATrs VecUtil ListUtil NatUtil RelUtil)