include "static_2/notation/functions/upspoon_2.ma".
(* SORT HIERARCHY ***********************************************************)
include "static_2/notation/functions/upspoon_2.ma".
(* SORT HIERARCHY ***********************************************************)