proposition: Lemma rStandardize n phi s : Proc phi -> rClosed phi s -> let (l,s') := (rCompSeval n (0,rCompClos s [])) in rPow phi l s (rDeClos s').
proof: Proof. Proof with eauto. intros pp cl. unfold rPow. rewrite rClosed_valid in *;auto. assert (cl': rValidComp phi (snd (rCompSeval n (0,rCompClos s [])))). - apply rCompSeval_rValidComp;auto. - destruct rCompSeval eqn:eq1. rewrite !expandDenote;auto. specialize (rCompSeval_sound n (rCompClos s []) 0 pp);intros H. rewrite eq1 in H. destruct H as [_ H]. rewrite Nat.sub_0_r in H. rewrite <- rDeClos_reduce... apply deClos_correct... destruct cl... Qed.
imports: Undecidability.L.Tactics(LClos) ZArith FunInd