-#I #G #L #V #U #T #HUT #U2 #HU2 elim (cpm_lifts_sn … HU2 (Ⓣ) … HUT) -U
-/3 width=9 by fqu_drop, drops_refl, drops_drop, ex3_2_intro/
+[ /5 width=5 by lsubr_cpm_trans, cpm_bind, lsubr_unit, fqu_clear, ex3_2_intro/
+| #I #G #L #U #T #HUT #U2 #HU2 elim (cpm_lifts_sn … HU2 (Ⓣ) … HUT) -U
+ /3 width=9 by fqu_drop, drops_refl, drops_drop, ex3_2_intro/
+]