#R #HR #T1 #T2 #HT12 #f #U1 #HTU1 #U2 #HTU2
elim (HR … HT12 … HTU1) -HR -T1 #X #HTX #HUX
<(lifts_mono … HTX … HTU2) -T2 -U2 -f //
#R #HR #T1 #T2 #HT12 #f #U1 #HTU1 #U2 #HTU2
elim (HR … HT12 … HTU1) -HR -T1 #X #HTX #HUX
<(lifts_mono … HTX … HTU2) -T2 -U2 -f //