proposition: Lemma rClosed_decb_correct phi s : Proc phi -> rClosed_decb s = true -> rClosed phi s.
proof: Proof. intros. hnf;split;[auto|]. rewrite closed_dcl. apply rClosed_decb'_correct;auto. Qed.
imports: Undecidability.L.Tactics(LClos) ZArith FunInd