proposition: Lemma rDeClos_reduce phi s: Proc phi -> rValidComp phi s -> deClos (denoteComp phi s) = deClos (denoteComp phi (rCompClos (rDeClos s) [])).
proof: Proof. intros pp vc. simpl. rewrite <- denoteTerm_correct;auto. now rewrite substList_nil. Qed.
imports: Undecidability.L.Tactics(LClos) ZArith FunInd