elim (lsubr_fwd_pair2 … H) -H #I2 #L2 #V2 #HL21 #H destruct
/3 width=3 by cpt_lref/
|6,11: /4 width=1 by cpg_bind, cpg_beta, lsubr_pair/
elim (lsubr_fwd_pair2 … H) -H #I2 #L2 #V2 #HL21 #H destruct
/3 width=3 by cpt_lref/
|6,11: /4 width=1 by cpg_bind, cpg_beta, lsubr_pair/