1. 15
  1.  

  2. 5

    Also worthy of note is Coq in a hurry where it goes on a little more about proofs on inductive proof principles by using the naturals and lists as examples. I used it when preparing my “Type theory and Coq” exam and things were rather pleasant after that except for some nasty functions which I couldn’t get to typecheck and I had to resort to Program Fixpoint to delay some proofs.