proposition: Lemma ren_cap_sub_aux : forall s t k l, exists s', ren_cap k (sub s t) = sub s' (ren_cap l t) /\ forall x, x < l \/ x >= l + nb_aliens t -> s' x = Var x.
proof: Proof. intros s t; pattern t; apply term_ind with (Q := fun n (ts : terms n) => forall k l, exists s', ren_caps k (Vmap (sub s) ts) = Vmap (sub s') (ren_caps l ts) /\ forall x, x < l \/ x >= l + nb_aliens_vec ts -> s' x = Var x); clear t; intros. simpl. single_tac l (ren_cap k (s x)). rewrite sub_fun, !ren_cap_fun, nb_aliens_fun. case (defined f R). simpl. single_tac l (@Var Sig k). destruct (H k l) as [s']. destruct H0. exists s'. rewrite H0, sub_fun. intuition. simpl. exists (fun x => Var x). auto. simpl. destruct (H k l) as [s1]. destruct H1 as [H1 H1']. rewrite H1. destruct (H0 (k + nb_aliens (sub s t)) (l + nb_aliens t)) as [s2]. destruct H2 as [H2 H2']. rewrite H2. set (s' := fun x => match In_dec x (vars (ren_cap l t)) with left _ => s1 x | right _ => s2 x end). exists s'. split. apply Vcons_eq_intro. apply sub_eq. intros. unfold s'. case (In_dec x (vars (ren_cap l t))); intro. refl. intuition. apply Vmap_sub_eq. intros. ded (vars_ren_caps H3). unfold s'. case (In_dec x (vars (ren_cap l t))); intro. ded (vars_ren_cap i). lia. refl. rewrite nb_aliens_cons. intros. unfold s'. case (In_dec x (vars (ren_cap l t))); intro. ded (vars_ren_cap i). lia. apply H2'. lia. Qed.
imports: CoLoR(LogicUtil ACalls ATrs VecUtil ListUtil NatUtil RelUtil)