Update dependent_type_theory.md

[newptcai]

The Nat does not need to be here if this is intended to show that Lean can infer types sometimes.

[david-christiansen]

Thanks!