+lemma lpx_sn_alt_intro_alt: ∀R,L1,L2. |L1| = |L2| →
+ (∀I1,I2,K1,K2,V1,V2,i.
+ ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
+ ∧∧ I1 = I2 & R K1 V1 V2 & lpx_sn_alt R K1 K2
+ ) → lpx_sn_alt R L1 L2.
+#R #L1 #L2 #HL12 #IH @lpx_sn_alt_intro // -HL12
+#I1 #I2 #K1 #K2 #V1 #V2 #i #HLK1 #HLK2
+elim (IH … HLK1 HLK2) -IH -HLK1 -HLK2 /2 width=1 by conj/
+qed.
+
+(* Basic forward lemmas ******************************************************)
+
+lemma lpx_sn_alt_fwd_length: ∀R,L1,L2. lpx_sn_alt R L1 L2 → |L1| = |L2|.
+#R #L1 #L2 #H elim (lpx_sn_alt_inv_alt … H) //
+qed-.
+
+(* Basic inversion lemmas ***************************************************)
+