End of afternoon -> Added admit for definitions and admitted fold_step. Also provided (hopefully) all the required theorems for the main proof. Evening -> defined foldl1 using proof and changed other theorem definitions accordingly