Nit: `Implicit Arguments` is deprecated, use `Arguments isp : clear implicits.` and `Arguments hproptype : clear implicits.`.