-fact lpx_sn_dropable_aux: ∀R,L2,K2,s,d,e. ⬇[s, d, e] L2 ≡ K2 → ∀L1. lpx_sn R L1 L2 →
- d = 0 → ∃∃K1. ⬇[s, 0, e] L1 ≡ K1 & lpx_sn R K1 K2.
-#R #L2 #K2 #s #d #e #H elim H -L2 -K2 -d -e
-[ #d #e #He #X #H >(lpx_sn_inv_atom2 … H) -H
+fact lpx_sn_dropable_aux: ∀R,L2,K2,s,l,m. ⬇[s, l, m] L2 ≡ K2 → ∀L1. lpx_sn R L1 L2 →
+ l = 0 → ∃∃K1. ⬇[s, 0, m] L1 ≡ K1 & lpx_sn R K1 K2.
+#R #L2 #K2 #s #l #m #H elim H -L2 -K2 -l -m
+[ #l #m #Hm #X #H >(lpx_sn_inv_atom2 … H) -H