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