--------------------- Implicit Coercions --------------------- :Source: https://coq.inria.fr/distrib/current/refman/coercions.html :Converted by: Maxime Dénès