+qed-.
+
+lemma fpcs_fwd_shift: ∀I,L1,L2,V1,V2,T1,T2. ⦃L1.ⓑ{I}V1, T1⦄ ⬌* ⦃L2.ⓑ{I}V2, T2⦄ →
+ ∀b. ⦃L1, ⓑ{b,I}V1.T1⦄ ⬌* ⦃L2, ⓑ{b,I}V2.T2⦄.
+/3 width=1 by fpcs_inv_shift, fpcs_fwd_bind_minus/ qed-.
+
+lemma fpcs_fwd_abst24: ∀a,L1,L2,V1,V2,T1,T2. ⦃L1, ⓛ{a}V1.T1⦄ ⬌* ⦃L2, ⓛ{a}V2.T2⦄ →
+ ∀b,I,W. ⦃L1, ⓑ{b,I}W.T1⦄ ⬌* ⦃L2, ⓑ{b,I}W.T2⦄.
+#a #L1 #L2 #V1 #V2 #T1 #T2 #H12 #b #I #W
+elim (fpcs_inv_fprs … H12) -H12 #L #U #H1 #H2
+elim (fprs_fwd_abst2 … H1 b I W) -H1 #W1 #U1 #HTU1 #H destruct
+elim (fprs_fwd_abst2 … H2 b I W) -H2 #W2 #U2 #HTU2 #H destruct /2 width=4/
+qed-.