In my searching, I've seen that if Church numerals are encoded in a dependently typed Lambda calculus, that we can't derive induction or that $0 \neq 1$.
I know that LF and the dependently typed Lambda calculus (from the Lambda cube) are often used to model logic, but any actual systems I've seen based on this augment it with inductive data types, propositional equality, etc.
I'm wondering, can anything non-trivial be done in a pure dependently typed Lambda calculus, without adding inductive types or such? I.e. is there anything we can encode (i.e. length indexed vectors, equality, etc) and prove things about in a dependently typed lambda system that we can't in a Simply Typed System, or something like System F?
I know that dependent types don't give us anything extra for computability, but I'm wondering about expressiveness.