// Iota-reduction is a rule in the Calculus of (Co-)Inductive Constructions,
// which "says that a destructor applied to an object built from a constructor
-// behaves as expected". -- https://web.archive.org/web/20100531091244/http://coq.inria.fr/doc/Reference-Manual006.html
+// behaves as expected". -- https://coq.inria.fr/doc/language/core/conversion.html#iota-reduction
//
// It's a little more complicated here, because of pointers and regions and
// trying to get assert failure messages that at least identify which case