proposition: Lemma vars_cap_sup : forall x t, In x (vars (cap t)) -> x > maxvar t -> In x (vars t) -> False.
proof: Proof. intros x t. pattern t. apply term_ind_forall; clear t; simpl; intros. intuition. change (In x (vars_vec v)) in H2. change (x > maxvars v) in H1. ded (in_vars_vec_elim H2). destruct H3 as [t]. destruct H3. ded (vars_max H4). ded (maxvar_in _ _ H5 H3). lia. Qed.
imports: Coq(Sumbool) CoLoR(LogicUtil ACalls ATrs VecUtil ListUtil NatUtil EqUtil)