[ #f1 #L1 #H12 #H1 #H2 destruct
/3 width=5 by lsubf_fwd_isid_dx, frees_unit/
| #f #f0 #f1 #J #L1 #V #H12 #Hf #Hf1 #H1 #H2 destruct
[ #f1 #L1 #H12 #H1 #H2 destruct
/3 width=5 by lsubf_fwd_isid_dx, frees_unit/
| #f #f0 #f1 #J #L1 #V #H12 #Hf #Hf1 #H1 #H2 destruct