-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.