-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
- /3 width=3 by inj, ex2_intro/
-| #K #K2 #_ #HK2 * #L #HL1 #HLK elim (HR … HLK … HK2) -HR -K
- /3 width=3 by step, ex2_intro/
-]
-qed-.
-