proposition: Lemma rReduceIntro phi l s t : Proc phi -> rClosed phi s -> rClosed phi t -> denoteTerm phi s >(l) denoteTerm phi t -> rPow phi l s t.
proof: Proof. unfold rPow;tauto. Qed.
imports: Undecidability.L.Tactics(LClos) ZArith FunInd