Use that in place of the old encoding: #70 (comment 52817)
Requires dropping support for Coq 8.7 (in a separate MR).