Came across the PFPL in Agda book, and tried it out for the first time: