Title: An example of algorithm development in Intuitionistic Type Theory