proposition: Lemma ren_caps_intro : forall n (ts : terms n) k, exists s, ts = Vmap (sub s) (ren_caps k ts) /\ forall x, x < k \/ x >= k + nb_aliens_vec ts -> s x = Var x.
proof: Proof. induction ts; intro. exists (fun x => Var x). intuition. simpl. destruct (ren_cap_intro h k) as [s1]. destruct H as [H1 H1']. destruct (IHts (k + nb_aliens h)) as [s2]. destruct H as [H2 H2']. set (s := fun x => match In_dec x (vars (ren_cap k h)) with | left _ => s1 x | right _ => s2 x end). exists s. assert (sub s (ren_cap k h) = sub s1 (ren_cap k h)). apply sub_eq. intros. unfold s. case (In_dec x (vars (ren_cap k h))); intro. refl. intuition. rewrite H, <- H1. assert (Vmap (sub s) (ren_caps (k + nb_aliens h) ts) = Vmap (sub s2) (ren_caps (k + nb_aliens h) ts)). apply Vmap_sub_eq. intros. ded (vars_ren_caps H0). unfold s. case (In_dec x (vars (ren_cap k h))); intro. ded (vars_ren_cap i). lia. refl. rewrite H0, <- H2. split. refl. rewrite nb_aliens_cons. intros. unfold s. case (In_dec x (vars (ren_cap k h))); intro. ded (vars_ren_cap i). lia. apply H2'. lia. Qed.
imports: CoLoR(LogicUtil ACalls ATrs VecUtil ListUtil NatUtil RelUtil)