-lemma llpx_sn_alt_r_bind: ∀R,a,I,L1,L2,V,T,d.
- llpx_sn_alt_r R d V L1 L2 →
- llpx_sn_alt_r R (⫯d) T (L1.ⓑ{I}V) (L2.ⓑ{I}V) →
- llpx_sn_alt_r R d (ⓑ{a,I}V.T) L1 L2.
-#R #a #I #L1 #L2 #V #T #d #HV #HT
+lemma llpx_sn_alt_r_bind: ∀R,a,I,L1,L2,V,T,l.
+ llpx_sn_alt_r R l V L1 L2 →
+ llpx_sn_alt_r R (⫯l) T (L1.ⓑ{I}V) (L2.ⓑ{I}V) →
+ llpx_sn_alt_r R l (ⓑ{a,I}V.T) L1 L2.
+#R #a #I #L1 #L2 #V #T #l #HV #HT