proposition: Lemma max_var_nformalae_correct : forall l p o v, In (p,o) l -> In v (vars xH p) -> Pos.le v (max_var_nformulae l)%positive.
proof: Proof. intros l p o v. apply max_var_nformulae_correct_aux. Qed.
imports: List Bool OrderedRing RingMicromega ZCoeff Refl ZArith_base ZArithRing Ztac EnvRing Coq.micromega.Tauto BinNums Zdiv Znumtheory QArith Znumtheory