+
+lemma co_dropable_dx_TC: ∀R. co_dropable_dx R → co_dropable_dx (LTC … R).
+#R #HR #f2 #L1 #L2 #H elim H -L2
+[ #L2 #HL12 #b #f #K2 #HLK2 #Hf #f1 #Hf2 elim (HR … HL12 … HLK2 … Hf … Hf2) -HR -Hf -f2 -L2
+ /3 width=3 by inj, ex2_intro/
+| #L #L2 #_ #HL2 #IHL1 #b #f #K2 #HLK2 #Hf #f1 #Hf2 elim (HR … HL2 … HLK2 … Hf … Hf2) -HR -L2
+ #K #HLK #HK2 elim (IHL1 … HLK … Hf … Hf2) -Hf -f2 -L
+ /3 width=5 by step, ex2_intro/
+]
+qed-.
+
+lemma co_dedropable_sn_TC: ∀R. co_dedropable_sn R → co_dedropable_sn (LTC … R).
+#R #HR #b #f #L1 #K1 #HLK1 #f1 #K2 #H elim H -K2
+[ #K2 #HK12 #f2 #Hf elim (HR … HLK1 … HK12 … Hf) -HR -f1 -K1
+ /3 width=4 by inj, ex3_intro/
+| #K #K2 #_ #HK2 #IH #f2 #Hf elim (IH … Hf) -IH -K1
+ #L #H1L1 #HLK #H2L1 elim (HR … HLK … HK2 … Hf) -HR -f1 -K
+ /3 width=6 by lreq_trans, step, ex3_intro/
+]
+qed-.