3 ms·

Dependent type literature will answer both of your questions relatively quickly. Also look at "proof search" in that context.