-lemma tw_shift: ∀L,T. #{L, T} ≤ #{L @@ T}.
-#L elim L //
-#K #I #V #IHL #T
-@transitive_le [3: @IHL |2: /2 width=2/ | skip ]
-qed.
-
-lemma fw_tpair_sn: ∀I,L,V,T. #{L, V} < #{L, ②{I}V.T}.
-normalize in ⊢ (?→?→?→?→?%%); //
-qed.
-
-lemma fw_tpair_dx: ∀I,L,V,T. #{L, T} < #{L, ②{I}V.T}.
-normalize in ⊢ (?→?→?→?→?%%); //
-qed.
-
-lemma fw_tpair_dx_sn: ∀I1,I2,L,V1,V2,T. #{L, V2} < #{L, ②{I1}V1.②{I2}V2.T}.
-normalize in ⊢ (?→?→?→?→?→?→?%%); /2 width=1/
+lemma fw_tpair_sn: ∀I,G,L,V,T. ♯{G, L, V} < ♯{G, L, ②{I}V.T}.
+normalize in ⊢ (?→?→?→?→?→?%%); //