lemma cnuw_inv_lifts (h) (G): d_deliftable1 … (cnuw h G).
#h #G #L #U #HU #b #f #K #HLK #T #HTU #n #T0 #H
elim (cpms_lifts_sn … H … HLK … HTU) -b -K #U0 #HTU0 #HU0
lemma cnuw_inv_lifts (h) (G): d_deliftable1 … (cnuw h G).
#h #G #L #U #HU #b #f #K #HLK #T #HTU #n #T0 #H
elim (cpms_lifts_sn … H … HLK … HTU) -b -K #U0 #HTU0 #HU0