This repo contains notes for my talk on "Inductive predicates" which I gave during a seminar called "Program certification in Coq" back in November 2017. They turned out to be a bit broader than just inductive predicates and cover all forms of structural induction, including functional induction, and even more, though they do not touch the topic of well-founded induction. Moreover, there's also some code, mainly small exercises, and one bigger file with a failed attempt at Robinson's unification algorithm, which I never fixed because of lack of time.
You can read everything in a nice, Software Foundations-like HTML version here