+interpretation "environment construction (binary)"
+ 'DxItem2 L I T = (LPair L I T).
+
+interpretation "environment binding construction (binary)"
+ 'DxBind2 L I T = (LPair L I T).
+
+interpretation "abbreviation (local environment)"
+ 'DxAbbr L T = (LPair L Abbr T).
+
+interpretation "abstraction (local environment)"
+ 'DxAbst L T = (LPair L Abst T).