proposition: Lemma ren_cap_idem : forall t k l, ren_cap k (ren_cap l t) = ren_cap k t.
proof: Proof. intro t; pattern t; apply term_ind with (Q := fun n (ts : terms n) => forall k l, ren_caps k (ren_caps l ts) = ren_caps k ts); clear t; intros; auto. rewrite !ren_cap_fun. case_eq (defined f R); intro H0. refl. rewrite ren_cap_fun, H0, H. refl. simpl. rewrite H, H0, nb_aliens_ren_cap. refl. Qed.
imports: CoLoR(LogicUtil ACalls ATrs VecUtil ListUtil NatUtil RelUtil)