interpretation "sort (global environment)"
'Star = (nil2 bind2 term).
-interpretation "environment binding construction (binary)"
+interpretation "global environment binding construction (binary)"
'DxBind2 L I T = (cons2 bind2 term I T L).
interpretation "abbreviation (global environment)"
(* Basic properties *********************************************************)
-axiom genv_eq_dec: ∀T1,T2:genv. Decidable (T1 = T2).
+axiom eq_genv_dec: ∀G1,G2:genv. Decidable (G1 = G2).