fact: Fixpoint boundb (k : nat) (t : term) : bool := match t with | var n => negb (k <=? n) | app s t => andb (boundb k s) (boundb k t) | lam s => boundb (S k) s end.
imports: Undecidability.L(Computability.Decidability Datatypes.LNat Datatypes.LTerm L) Nat