(* WEIGHT OF A GLOBAL ENVIRONMENT *******************************************)
rec definition gw G ≝ match G with
-[ GAtom ⇒ 0
-| GPair G I T ⇒ gw G + ♯{T}
+[ GAtom ⇒ 𝟏
+| GPair G I T ⇒ gw G + ♯❨T❩
].
interpretation "weight (global environment)" 'Weight G = (gw G).
(* Basic properties *********************************************************)
-lemma gw_pair: ∀I,G,T. ♯{G} < ♯{G.ⓑ{I}T}.
-normalize /2 width=1 by monotonic_le_plus_r/ qed.
+lemma gw_atom_unfold: 𝟏 = ♯❨⋆❩.
+// qed.
+
+lemma gw_pair_unfold (I) (G) (T): ♯❨G❩ + ♯❨T❩ = ♯❨G.ⓑ[I]T❩.
+// qed.
+
+lemma gw_pair: ∀I,G,T. ♯❨G❩ < ♯❨G.ⓑ[I]T❩.
+// qed.