#h #G #L #U1 #U2 * #cU #HU12 #b #f #K #HLK #T1 #HTU1
elim (cpg_inv_lifts_sn … HU12 … HLK … HTU1) -L -U1
/3 width=4 by ex2_intro, ex_intro/
qed-.
#h #G #L #U1 #U2 * #cU #HU12 #b #f #K #HLK #T1 #HTU1
elim (cpg_inv_lifts_sn … HU12 … HLK … HTU1) -L -U1
/3 width=4 by ex2_intro, ex_intro/
qed-.