Agda Playground I'm progressing through PLFA and writing these proofs. Part 1 Naturals Induction Relations Equality Isomorphism + ℕ-CanBin isomorphism Connectives Negation Quantifiers Decidable Lists Part 2 Lambda Properties Part 3