include "static_2/syntax/genv.ma".
(* LENGTH OF A GLOBAL ENVIRONMENT *******************************************)
rec definition glength G on G ≝ match G with
include "static_2/syntax/genv.ma".
(* LENGTH OF A GLOBAL ENVIRONMENT *******************************************)
rec definition glength G on G ≝ match G with