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