proposition: Lemma rClosed_valid s phi : Proc phi -> (rClosed phi s <-> rValidComp phi (rCompClos s [])).
proof: Proof. intros pp. unfold rClosed. unfold rValidComp. rewrite closed_dcl. split;intros H. - repeat constructor;simpl;intuition;apply H0. - inv H. inv H1. now tauto. Qed.
imports: Undecidability.L.Tactics(LClos) ZArith FunInd