To explain in simpler terms, what you do is promote values to types first. I.e. when a user enters a string, you have to somehow prove, using formal logic, that n < l. After that, the proof is encoded in the types and you can use functions as ngram above that depend on this proof.