+lemma lleq_lift_le: ∀K1,K2,T,d0. K1 ⋕[d0, T] K2 →
+ ∀L1,L2,d,e. ⇩[d, e] L1 ≡ K1 → ⇩[d, e] L2 ≡ K2 →
+ ∀U. ⇧[d, e] T ≡ U → d0 ≤ d → L1 ⋕[d0, U] L2.
+#K1 #K2 #T #d0 #H elim H -K1 -K2 -T -d0
+[ #K1 #K2 #d0 #k #HK12 #L1 #L2 #d #e #HLK1 #HLK2 #X #H #_ >(lift_inv_sort1 … H) -X
+ lapply (ldrop_fwd_length_eq2 … HLK1 HLK2 HK12) -K1 -K2 -d
+ /2 width=1 by lleq_sort/
+| #I1 #I2 #K1 #K2 #K11 #K22 #V1 #V2 #d0 #i #Hid0 #HK11 #HK22 #_ #_ #IHV1 #IHV2 #L1 #L2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_lref1 … H) -H
+ * #Hdi #H destruct
+ [ elim (ldrop_trans_lt … HLK1 … HK11) // -K1
+ elim (ldrop_trans_lt … HLK2 … HK22) // -K2
+ #K2 #W2 #HLK2 #HK22 #HVW2 #K1 #W1 #HLK1 #HK11 #HVW1 -Hdi
+ @(lleq_skip … HLK1 HLK2) // /3 width=6 by monotonic_le_minus_l2/ (**) (* full auto fails *)
+ | elim (lt_refl_false i) -I1 -I2 -L1 -L2 -K1 -K2 -K11 -K22 -V1 -V2 -e
+ /3 width=3 by lt_to_le_to_lt, transitive_le/ (**) (* slow *)
+ ]
+| #I #K1 #K2 #K11 #K22 #V #d0 #i #Hid0 #HK11 #HK22 #HV #IHV #L1 #L2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_lref1 … H) -H
+ * #Hdi #H destruct [ -HV | -IHV ]
+ [ elim (ldrop_trans_lt … HLK1 … HK11) // -K1 #K1 #W #HLK1 #HK11 #HVW
+ elim (ldrop_trans_lt … HLK2 … HK22) // -Hdi -K2 #K2 #W2 #HLK2 #HK22 #HVW2
+ lapply (lift_mono … HVW2 … HVW) -HVW2 #H destruct /3 width=12 by lleq_lref/
+ | lapply (ldrop_trans_ge … HLK1 … HK11 ?) // -K1
+ lapply (ldrop_trans_ge … HLK2 … HK22 ?) // -Hdi -K2
+ /3 width=7 by lleq_lref, transitive_le/
+ ]
+| #K1 #K2 #d0 #i #HK1 #HK2 #HK12 #L1 #L2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_lref1 … H) -H
+ * #Hid #H destruct
+ lapply (ldrop_fwd_length_eq2 … HLK1 HLK2 HK12) -HK12
+ [ /3 width=6 by lleq_free, ldrop_fwd_be/
+ | lapply (ldrop_fwd_length … HLK1) -HLK1 #HLK1
+ lapply (ldrop_fwd_length … HLK2) -HLK2 #HLK2
+ @lleq_free [ >HLK1 | >HLK2 ] -Hid -HLK1 -HLK2 /2 width=1 by monotonic_le_plus_r/ (**) (* explicit constructor *)
+ ]
+| #K1 #K2 #d0 #p #HK12 #L1 #L2 #d #e #HLK1 #HLK2 #X #H #_ >(lift_inv_gref1 … H) -X
+ lapply (ldrop_fwd_length_eq2 … HLK1 HLK2 HK12) -K1 -K2 -d -e
+ /2 width=1 by lleq_gref/
+| #a #I #K1 #K2 #V #T #d0 #_ #_ #IHV #IHT #L1 #L2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_bind1 … H) -H
+ #W #U #HVW #HTU #H destruct /4 width=6 by lleq_bind, ldrop_skip, le_S_S/
+| #I #K1 #K2 #V #T #d0 #_ #_ #IHV #IHT #L1 #L2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_flat1 … H) -H
+ #W #U #HVW #HTU #H destruct /3 width=6 by lleq_flat/
+]
+qed-.
+
+lemma lleq_lift_ge: ∀K1,K2,T,d0. K1 ⋕[d0, T] K2 →
+ ∀L1,L2,d,e. ⇩[d, e] L1 ≡ K1 → ⇩[d, e] L2 ≡ K2 →
+ ∀U. ⇧[d, e] T ≡ U → d ≤ d0 → L1 ⋕[d0+e, U] L2.
+#K1 #K2 #T #d0 #H elim H -K1 -K2 -T -d0
+[ #K1 #K2 #d0 #k #HK12 #L1 #L2 #d #e #HLK1 #HLK2 #X #H #_ >(lift_inv_sort1 … H) -X
+ lapply (ldrop_fwd_length_eq2 … HLK1 HLK2 HK12) -K1 -K2 -d
+ /2 width=1 by lleq_sort/
+| #I1 #I2 #K1 #K2 #K11 #K22 #V1 #V2 #d0 #i #hid0 #HK11 #HK22 #HV1 #HV2 #IHV1 #IHV2 #L1 #L2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_lref1 … H) -H
+ * #Hdi #H destruct [ -HV1 -HV2 | -IHV1 -IHV2 ]
+ [ elim (ldrop_trans_lt … HLK1 … HK11) // -K1 #K1 #W1 #HLK1 #HK11 #HVW1
+ elim (ldrop_trans_lt … HLK2 … HK22) // -K2 #K2 #W2 #HLK2 #HK22 #HVW2
+ @(lleq_skip … HLK1 HLK2) -HLK1 -HLK2 (**) (* explicit constructor *)
+ [ /2 width=3 by lt_to_le_to_lt/ ]
+ >arith_i /3 width=5 by monotonic_le_minus_l2/
+ | lapply (ldrop_trans_ge_comm … HLK1 … HK11 ?) // -K1
+ lapply (ldrop_trans_ge_comm … HLK2 … HK22 ?) // -K2
+ /4 width=10 by lleq_skip, monotonic_lt_plus_l/
+ ]
+| #I #K1 #K2 #K11 #K22 #V #d0 #i #Hid0 #HK11 #HK22 #HV #_ #L1 #L2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_lref1 … H) -H
+ * #Hid #H destruct
+ [ elim (lt_refl_false i) -I -L1 -L2 -K1 -K2 -K11 -K22 -V -e
+ /3 width=3 by lt_to_le_to_lt, transitive_le/ (**) (* slow *)
+ | lapply (ldrop_trans_ge … HLK1 … HK11 ?) // -K1
+ lapply (ldrop_trans_ge … HLK2 … HK22 ?) // -Hid -K2
+ /3 width=7 by lleq_lref, monotonic_le_plus_l/
+ ]
+| #K1 #K2 #d0 #i #HK1 #HK2 #HK12 #L1 #L2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_lref1 … H) -H
+ * #Hid #H destruct
+ lapply (ldrop_fwd_length_eq2 … HLK1 HLK2 HK12) -HK12
+ [ /3 width=6 by lleq_free, ldrop_fwd_be/
+ | lapply (ldrop_fwd_length … HLK1) -HLK1 #HLK1
+ lapply (ldrop_fwd_length … HLK2) -HLK2 #HLK2
+ @lleq_free [ >HLK1 | >HLK2 ] -Hid -HLK1 -HLK2 /2 width=1 by monotonic_le_plus_r/ (**) (* explicit constructor *)
+ ]
+| #K1 #K2 #d0 #p #HK12 #L1 #L2 #d #e #HLK1 #HLK2 #X #H #_ >(lift_inv_gref1 … H) -X
+ lapply (ldrop_fwd_length_eq2 … HLK1 HLK2 HK12) -K1 -K2 -d
+ /2 width=1 by lleq_gref/
+| #a #I #K1 #K2 #V #T #d0 #_ #_ #IHV #IHT #L1 #L2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_bind1 … H) -H
+ #W #U #HVW #HTU #H destruct /4 width=5 by lleq_bind, ldrop_skip, le_minus_to_plus/
+| #I #K1 #K2 #V #T #d0 #_ #_ #IHV #IHT #L1 #L2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_flat1 … H) -H
+ #W #U #HVW #HTU #H destruct /3 width=5 by lleq_flat/
+]
+qed-.
+
+lemma lleq_be: ∀L1,L2,U,d0. L1 ⋕[d0, U] L2 →
+ ∀K1,K2,d,e. ⇩[d, e] L1 ≡ K1 → ⇩[d, e] L2 ≡ K2 →
+ ∀T. ⇧[d, e] T ≡ U → d ≤ d0 → d0 ≤ d + e → L1 ⋕[d, U] L2.
+#L1 #L2 #U #d0 #H elim H -L1 -L2 -U -d0
+/2 width=1 by lleq_sort, lleq_free, lleq_gref/
+[ #I1 #I2 #L1 #L2 #K11 #K22 #W1 #W2 #d0 #i #Hid0 #HLK11 #HLK22 #_ #_ #IHW1 #IHW2 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 #Hd0de elim (lift_inv_lref2 … H) -H
+ * #Hid #H destruct [ -Hid0 | -Hd0 ]
+ [ elim (ldrop_conf_lt … HLK1 … HLK11) // -HLK1
+ elim (ldrop_conf_lt … HLK2 … HLK22) // -HLK2
+ #L2 #V2 #_ #HKL22 #HVW2 #L1 #V1 #_ #HKL21 #HVW1
+ @(lleq_skip … HLK11 HLK22) -HLK11 -HLK22 //
+ /3 width=8 by arith_k_dx, monotonic_le_minus_l2/ (**) (* full auto fails *)
+ | -I1 -I2 -K11 -K22 -K1 -K2 -W1 -W2 elim (lt_refl_false … i) -L1 -L2
+ @(lt_to_le_to_lt … Hid0) -Hid0 /2 width=3 by transitive_le/ (**) (* full auto too slow *)
+ ]
+| #I #L1 #L2 #K11 #K22 #W #d0 #i #Hid0 #HLK11 #HLK22 #HW #_ #K1 #K2 #d #e #_ #_ #X #H #Hd0 #_ elim (lift_inv_lref2 … H) -H
+ * #Hid #H destruct
+ [ -I -K1 -K2 -K11 -K22 -W elim (lt_refl_false i)
+ @(lt_to_le_to_lt … Hid) -Hid /2 width=3 by transitive_le/ (**) (* full auto too slow *)
+ | -d0 /3 width=7 by lleq_lref, le_plus_b/
+ ]
+| #a #I #L1 #L2 #W #U #d0 #_ #_ #IHW #IHU #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 #Hde elim (lift_inv_bind2 … H) -H
+ #V #T #HVW #HTU #H destruct
+ @lleq_bind [ /2 width=8 by/ ] -IHW
+ @(IHU … HTU) -IHU -HTU /2 width=2 by ldrop_skip, le_S_S/ (**) (* full auto too slow *)
+| #I #L1 #L2 #W #U #d0 #_ #_ #IHW #IHU #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 #Hde elim (lift_inv_flat2 … H) -H
+ #V #T #HVW #HTU #H destruct /3 width=8 by lleq_flat/
+]
+qed-.
+
+axiom- lleq_dec: ∀T,L1,L2,d. Decidable (L1 ⋕[d, T] L2).
+(*