proposition: Lemma vars_cap : forall x t, In x (vars (cap t)) -> x <= maxvar t + nb_aliens t.
proof: Proof. intros. apply vars_fcap_fresh. apply Nat.le_refl. rewrite cap_eq in H. hyp. Qed.
imports: Coq(Sumbool) CoLoR(LogicUtil ACalls ATrs VecUtil ListUtil NatUtil EqUtil)