proposition: Lemma closedb_spec s : Bool.reflect (closed s) (closedb s).
proof: Proof. unfold closedb. destruct (boundb_spec 0 s);constructor; rewrite closed_dcl;auto. Qed.
imports: Undecidability.L(Computability.Decidability Datatypes.LNat Datatypes.LTerm L) Nat