proposition: Lemma boundb_spec k t : Bool.reflect (bound k t) (boundb k t).
proof: Proof. revert k. induction t;intros;cbn. simpl. - destruct (Nat.leb_spec0 k n); simpl;constructor. intros H. inv H. lia. constructor. lia. - specialize (IHt1 k). specialize (IHt2 k). inv IHt1;simpl. + inv IHt2;constructor. * now constructor. * intros C. now inv C. + constructor. intros C. now inv C. - specialize (IHt (S k)). inv IHt;constructor. + now constructor. + intros C. now inv C. Qed.
imports: Undecidability.L(Computability.Decidability Datatypes.LNat Datatypes.LTerm L) Nat