proposition: Lemma rStandardizeUse n phi s: Proc phi -> rClosed phi s -> let (l,s') := (rCompSeval n (0,rCompClos s [])) in denoteTerm phi s >* denoteTerm phi (rDeClos s').
proof: Proof. intros a b. specialize (rStandardizeUsePow n a b). destruct (rCompSeval _ _). rewrite star_pow. firstorder. Qed.
imports: Undecidability.L.Tactics(LClos) ZArith FunInd