Fix #70: add pattern variant of bind notation

Use that in place of the old encoding: #70 (comment 52817)

Requires dropping support for Coq 8.7 (in a separate MR).