proposition: Lemma vars_fcap_fresh : forall x t m, maxvar t <= m -> In x (vars (fcap (capa t) (fresh (S m) (nb_aliens t)))) -> x <= m + nb_aliens t.
proof: Proof. intro. set (Q := fun n (ts : terms n) => forall m, maxvars ts <= m -> In x (vars_vec (Vmap_sum (Vmap capa ts) (fresh (S m) (sum (Vmap capa ts))))) -> x <= m + sum (Vmap capa ts)). intro. pattern t. apply term_ind with (Q := Q); clear t. simpl. intros. destruct H0. subst x0. lia. contr. intros f ts H m H0. unfold nb_aliens. simpl. case (defined f R); simpl; intros. destruct H1. lia. contr. apply H; hyp. unfold Q. simpl. intros. contr. intros. unfold Q. simpl. intros m H1. rewrite fresh_plus, Vbreak_app. simpl. intro. ded (in_app_or H2). destruct H3. assert (x <= m + projT1 (capa t)). apply H. eapply le_max_elim_l. rewrite maxvars_cons in H1. apply H1. hyp. lia. rewrite Nat.add_assoc. apply H0. assert (maxvars v <= m). eapply le_max_elim_r. rewrite maxvars_cons in H1. apply H1. lia. hyp. Qed.
imports: Coq(Sumbool) CoLoR(LogicUtil ACalls ATrs VecUtil ListUtil NatUtil EqUtil)