Should be nearly completed report for DTP.
It includes some TODOs that are mostly about theorem proving
And a todo about doing some research after well-founded recursion.
The report contains a list of files to be sent along with report,
the files FoldStep.v and Function.v are confirmed and should be sent
along with the report in the current state.