proposition: Lemma ren_cap_fun : forall f ts k, ren_cap k (Fun f ts) = if defined f R then Var k else Fun f (ren_caps k ts).
proof: Proof. intros. unfold ren_cap, nb_aliens. simpl. case (defined f R). refl. unfold fcap. simpl. apply args_eq. apply ren_caps_eq. Qed.
imports: CoLoR(LogicUtil ACalls ATrs VecUtil ListUtil NatUtil RelUtil)