#h #o #G #L #U #H @(rdsx_ind … H) -L
#L1 #_ #IH #b #f #K1 #HLK1 #Hf #T #HTU @rdsx_intro
#K2 #HK12 #HnK12 elim (drops_lpx_trans … HLK1 … HK12) -HK12
#h #o #G #L #U #H @(rdsx_ind … H) -L
#L1 #_ #IH #b #f #K1 #HLK1 #Hf #T #HTU @rdsx_intro
#K2 #HK12 #HnK12 elim (drops_lpx_trans … HLK1 … HK12) -HK12