1 free point +


1.1

1p for pure_bind
1p for bind_pure
1p for bind_assoc

2.1

2p
  0.5p for first equation
  0.5p for second equation
  1.0p for third equation

2.2

2p
  0.5p for first equation
  0.5p for second equation
  1.0p for third equation

2.3

2p
  -1p if the lemma doesn't hold
  -1p if half-finished (up to one IH application)


Comments:

  * how to unfold >>=
    * unfold has_bind.bind
    * simp [(>>=)]
    * show/change
  * if cases is too weak, do an induction!
  * option semantics cheating
