proposition: Lemma rClosed_decb'_correct s phi n: Proc phi -> rClosed_decb' n s = true -> bound n (denoteTerm phi s).
proof: Proof. intros pp. revert n. induction s;intros n eq;simpl in *. - rewrite Bool.negb_true_iff in eq. apply leb_complete_conv in eq. now constructor. - rewrite Bool.andb_true_iff in eq. constructor; intuition. - constructor. auto. - apply bound_ge with (k:=0);[|lia]. rewrite <- closed_dcl. apply pp. - unfold rho,r. repeat (eapply dclApp||eapply dcllam||eapply dclvar). all:try lia. eauto. Qed.
imports: Undecidability.L.Tactics(LClos) ZArith FunInd