proposition: Lemma rStandardizeUsePow n phi s: Proc phi -> rClosed phi s -> let (l,s') := (rCompSeval n (0,rCompClos s [])) in denoteTerm phi s >(l) denoteTerm phi (rDeClos s').
proof: Proof. apply rStandardize. Qed.
imports: Undecidability.L.Tactics(LClos) ZArith FunInd