+qed-.
+
+lemma lleq_llpx_sn_conf: ∀R. lleq_transitive R →
+ ∀L1,L2,T,d. L1 ⋕[T, d] L2 →
+ ∀L. llpx_sn R d T L1 L → llpx_sn R d T L2 L.
+/3 width=3 by lleq_llpx_sn_trans, lleq_sym/ qed-.
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma lleq_inv_lref_ge_dx: ∀L1,L2,d,i. L1 ⋕[#i, d] L2 → d ≤ i →
+ ∀I,K2,V. ⇩[i] L2 ≡ K2.ⓑ{I}V →
+ ∃∃K1. ⇩[i] L1 ≡ K1.ⓑ{I}V & K1 ⋕[V, 0] K2.
+#L1 #L2 #d #i #H #Hdi #I #K2 #V #HLK2 elim (llpx_sn_inv_lref_ge_dx … H … HLK2) -L2
+/2 width=3 by ex2_intro/
+qed-.
+
+lemma lleq_inv_lref_ge_sn: ∀L1,L2,d,i. L1 ⋕[#i, d] L2 → d ≤ i →
+ ∀I,K1,V. ⇩[i] L1 ≡ K1.ⓑ{I}V →
+ ∃∃K2. ⇩[i] L2 ≡ K2.ⓑ{I}V & K1 ⋕[V, 0] K2.
+#L1 #L2 #d #i #H #Hdi #I1 #K1 #V #HLK1 elim (llpx_sn_inv_lref_ge_sn … H … HLK1) -L1
+/2 width=3 by ex2_intro/
+qed-.
+
+lemma lleq_inv_lref_ge_bi: ∀L1,L2,d,i. L1 ⋕[#i, d] L2 → d ≤ i →
+ ∀I1,I2,K1,K2,V1,V2.
+ ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
+ ∧∧ I1 = I2 & K1 ⋕[V1, 0] K2 & V1 = V2.
+/2 width=8 by llpx_sn_inv_lref_ge_bi/ qed-.
+
+lemma lleq_inv_lref_ge: ∀L1,L2,d,i. L1 ⋕[#i, d] L2 → d ≤ i →
+ ∀I,K1,K2,V. ⇩[i] L1 ≡ K1.ⓑ{I}V → ⇩[i] L2 ≡ K2.ⓑ{I}V →
+ K1 ⋕[V, 0] K2.
+#L1 #L2 #d #i #HL12 #Hdi #I #K1 #K2 #V #HLK1 #HLK2
+elim (lleq_inv_lref_ge_bi … HL12 … HLK1 HLK2) //
+qed-.
+
+lemma lleq_inv_S: ∀L1,L2,T,d. L1 ⋕[T, d+1] L2 →
+ ∀I,K1,K2,V. ⇩[d] L1 ≡ K1.ⓑ{I}V → ⇩[d] L2 ≡ K2.ⓑ{I}V →
+ K1 ⋕[V, 0] K2 → L1 ⋕[T, d] L2.
+/2 width=9 by llpx_sn_inv_S/ qed-.
+
+lemma lleq_inv_bind_O: ∀a,I,L1,L2,V,T. L1 ⋕[ⓑ{a,I}V.T, 0] L2 →
+ L1 ⋕[V, 0] L2 ∧ L1.ⓑ{I}V ⋕[T, 0] L2.ⓑ{I}V.
+/2 width=2 by llpx_sn_inv_bind_O/ qed-.
+
+(* Advanced forward lemmas **************************************************)
+
+lemma lleq_fwd_lref_dx: ∀L1,L2,d,i. L1 ⋕[#i, d] L2 →
+ ∀I,K2,V. ⇩[i] L2 ≡ K2.ⓑ{I}V →
+ i < d ∨
+ ∃∃K1. ⇩[i] L1 ≡ K1.ⓑ{I}V & K1 ⋕[V, 0] K2 & d ≤ i.
+#L1 #L2 #d #i #H #I #K2 #V #HLK2 elim (llpx_sn_fwd_lref_dx … H … HLK2) -L2
+[ | * ] /3 width=3 by ex3_intro, or_intror, or_introl/
+qed-.