#a #I #L1 #L2 #V #T #d * #HL12 #IHV * #_ #IHT @conj // -HL12
#X @conj #H elim (cpys_inv_bind1 … H) -H
#W #U #HVW #HTU #H destruct
-elim (IHV W) -IHV #H1VW #H1WV
-elim (IHT U) -IHT #H1TU #H1UT
-@cpys_bind /2 width=1 by/ -HVW -H1VW -H1WV
-[ @(lsuby_cpys_trans … (L2.ⓑ{I}V))
-| @(lsuby_cpys_trans … (L1.ⓑ{I}V))
-] /4 width=5 by lsuby_cpys_trans, lsuby_succ/ (**) (* full auto too slow *)
+elim (IHV W) -IHV elim (IHT U) -IHT /3 width=1 by cpys_bind/
qed.
lemma lleq_flat: ∀I,L1,L2,V,T,d.
#HU0 elim (cpys_up … HU0 … HTU) // -HU0 /4 width=5 by cpys_weak/
qed-.
+lemma lsuby_lleq_trans: ∀L2,L,T,d. L2 ⋕[T, d] L →
+ ∀L1. L1 ⊑×[d, ∞] L2 → |L1| = |L2| → L1 ⋕[T, d] L.
+#L2 #L #T #d * #HL2 #IH #L1 #HL12 #H @conj // -HL2
+#U elim (IH U) -IH #Hdx #Hsn @conj #HTU
+[ @Hdx -Hdx -Hsn @(lsuby_cpys_trans … HTU) -HTU
+ /2 width=1 by lsuby_sym/ (**) (* full auto does not work *)
+| -H -Hdx /3 width=3 by lsuby_cpys_trans/
+]
+qed-.
+
+lemma lleq_lsuby_trans: ∀L,L1,T,d. L ⋕[T, d] L1 →
+ ∀L2. L1 ⊑×[d, ∞] L2 → |L1| = |L2| → L ⋕[T, d] L2.
+/5 width=4 by lsuby_lleq_trans, lleq_sym, lsuby_sym/ qed-.
+
+lemma lleq_lsuby_repl: ∀L1,L2,T,d. L1 ⋕[T, d] L2 →
+ ∀K1. K1 ⊑×[d, ∞] L1 → |K1| = |L1| →
+ ∀K2. L2 ⊑×[d, ∞] K2 → |L2| = |K2| →
+ K1 ⋕[T, d] K2.
+/3 width=4 by lleq_lsuby_trans, lsuby_lleq_trans/ qed-.
+
(* Basic forward lemmas *****************************************************)
lemma lleq_fwd_length: ∀L1,L2,T,d. L1 ⋕[T, d] L2 → |L1| = |L2|.
#L1 #L2 #T #d * //
qed-.
-lemma lleq_fwd_ldrop_sn: ∀L1,L2,T,d. L1 ⋕[d, T] L2 → ∀K1,i. ⇩[0, i] L1 ≡ K1 →
- ∃K2. ⇩[0, i] L2 ≡ K2.
+lemma lleq_fwd_ldrop_sn: ∀L1,L2,T,d. L1 ⋕[d, T] L2 → ∀K1,i. ⇩[i] L1 ≡ K1 →
+ ∃K2. ⇩[i] L2 ≡ K2.
#L1 #L2 #T #d #H #K1 #i #HLK1 lapply (lleq_fwd_length … H) -H
#HL12 lapply (ldrop_fwd_length_le2 … HLK1) -HLK1 /2 width=1 by ldrop_O1_le/
qed-.
-lemma lleq_fwd_ldrop_dx: ∀L1,L2,T,d. L1 ⋕[d, T] L2 → ∀K2,i. ⇩[0, i] L2 ≡ K2 →
- ∃K1. ⇩[0, i] L1 ≡ K1.
+lemma lleq_fwd_ldrop_dx: ∀L1,L2,T,d. L1 ⋕[d, T] L2 → ∀K2,i. ⇩[i] L2 ≡ K2 →
+ ∃K1. ⇩[i] L1 ≡ K1.
/3 width=6 by lleq_fwd_ldrop_sn, lleq_sym/ qed-.
lemma lleq_fwd_bind_sn: ∀a,I,L1,L2,V,T,d.