Transform slides to handouts for Lecture5
Add slides for Lecture 6
Add supplementary reading
Add Coq script related to inductive datatypes and induction