proposition: Lemma ren_cap_sub : forall s t k, exists s', ren_cap k (sub s t) = sub s' (ren_cap k t) /\ forall x, x < k \/ x >= k + nb_aliens t -> s' x = Var x.
proof: Proof. intros. apply ren_cap_sub_aux with (l := k). Qed.
imports: CoLoR(LogicUtil ACalls ATrs VecUtil ListUtil NatUtil RelUtil)