#I #K #V #HLK lapply (csx_inv_lref_bind … HLK … H) -H
/4 width=6 by lsx_lref_be, fqup_lref/
| #a #I #V #T #HG #HL #HT #H #d destruct
#I #K #V #HLK lapply (csx_inv_lref_bind … HLK … H) -H
/4 width=6 by lsx_lref_be, fqup_lref/
| #a #I #V #T #HG #HL #HT #H #d destruct