elim (IHU1 … HLK … HTU1) -IHU1 -U1 #T #HTU #HT1
elim (HR … HU2 … HLK … HTU) -HR -L -U /3 width=5 by lstar_dx, ex2_intro/
]
qed-.
lemma dropable_dx_TC: ∀R. dropable_dx R → dropable_dx (LTC … R).
elim (IHU1 … HLK … HTU1) -IHU1 -U1 #T #HTU #HT1
elim (HR … HU2 … HLK … HTU) -HR -L -U /3 width=5 by lstar_dx, ex2_intro/
]
qed-.
lemma dropable_dx_TC: ∀R. dropable_dx R → dropable_dx (LTC … R).