proposition: Lemma rDeClos_rValidComp phi s: Proc phi -> rValidComp phi s -> rValidComp phi (rCompClos (rDeClos s) []).
proof: Proof. Proof with repeat (eauto || congruence || subst || simpl in * || intuition). intros pp [? H]. unfold rValidComp in *. split;try tauto. simpl. apply deClos_valComp in H. apply validComp_closed. now rewrite <- denoteTerm_correct. Qed.
imports: Undecidability.L.Tactics(LClos) ZArith FunInd