A definition of step using a decreasing natural number that should be >= to the length of the input list
Solving fold_step_not_nil and fold_step_inc should be possible now, however I dont see / know the tactics to do it. I will ask Wouter on tuesday.