proposition: Lemma vars_fcap_fresh_inf : forall x t m, maxvar t <= m -> In x (vars (fcap (capa t) (fresh (S m) (nb_aliens t)))) -> x <= m -> In x (vars 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 -> In x (vars_vec ts)). intro. pattern t. apply term_ind with (Q := Q); clear t; intros. hyp. rewrite vars_fun. unfold nb_aliens in H1. simpl in H1. destruct (defined f R); simpl in H1. destruct H1. absurd (x<=m); lia. contr. apply H with (m := m); hyp. unfold Q. simpl. intros. contr. unfold Q. simpl. set (m := max (maxvar t) (maxvars v)). intros m0 H1. rewrite fresh_plus, Vbreak_app. simpl. intros. ded (in_app_or H2). destruct H4. apply in_appl. apply H with (m := m0). eapply le_max_elim_l. unfold m in H1. rewrite maxvars_cons in H1. apply H1. unfold nb_aliens. hyp. hyp. apply in_appr. unfold Q in H0. apply H0 with (m := m0 + projT1 (capa t)). assert (maxvars v <= m0). eapply le_max_elim_r. unfold m in H1. rewrite maxvars_cons in H1. apply H1. lia. hyp. lia. Qed.
imports: Coq(Sumbool) CoLoR(LogicUtil ACalls ATrs VecUtil ListUtil NatUtil EqUtil)