#h #G #K #T #HT #b #f #L #HLK #U #HTU #U0 #H
elim (cpm_inv_lifts_sn ā¦ H ā¦ HLK ā¦ HTU) -b -L #T0 #HTU0 #HT0
lapply (HT ā¦ HT0) -G -K #H destruct /2 width=4 by lifts_mono/
#h #G #K #T #HT #b #f #L #HLK #U #HTU #U0 #H
elim (cpm_inv_lifts_sn ā¦ H ā¦ HLK ā¦ HTU) -b -L #T0 #HTU0 #HT0
lapply (HT ā¦ HT0) -G -K #H destruct /2 width=4 by lifts_mono/