/3 width=3 by leq_sym, ex2_intro/
qed-.
+lemma ldrop_O1_ex: ∀K2,i,L1. |L1| = |K2| + i →
+ ∃∃L2. L1 ≃[0, i] L2 & ⇩[i] L2 ≡ K2.
+#K2 #i @(nat_ind_plus … i) -i
+[ /3 width=3 by leq_O2, ex2_intro/
+| #i #IHi #Y #Hi elim (ldrop_O1_lt Y 0) //
+ #I #L1 #V #H lapply (ldrop_inv_O2 … H) -H #H destruct
+ normalize in Hi; elim (IHi L1) -IHi
+ /3 width=5 by ldrop_drop, leq_pair, injective_plus_l, ex2_intro/
+]
+qed-.
+
lemma dedropable_sn_TC: ∀R. dedropable_sn R → dedropable_sn (TC … R).
#R #HR #L1 #K1 #s #d #e #HLK1 #K2 #H elim H -K2
[ #K2 #HK12 elim (HR … HLK1 … HK12) -HR -K1
(* Inversion lemmas on equivalence ******************************************)
-lemma ldrop_O_inj: ∀i,L1,L2,K. ⇩[i] L1 ≡ K → ⇩[i] L2 ≡ K → L1 ≃[i, ∞] L2.
+lemma ldrop_O1_inj: ∀i,L1,L2,K. ⇩[i] L1 ≡ K → ⇩[i] L2 ≡ K → L1 ≃[i, ∞] L2.
#i @(nat_ind_plus … i) -i
[ #L1 #L2 #K #H <(ldrop_inv_O2 … H) -K #H <(ldrop_inv_O2 … H) -L1 //
| #i #IHi * [2: #L1 #I1 #V1 ] * [2,4: #L2 #I2 #V2 ] #K #HLK1 #HLK2 //