[ lapply (lstas_inv_O … H2) -H2 #H destruct // ]
elim (snv_inv_lref … H1) -H1 #I0 #K0 #X0 #HLK0 #HX0
elim (da_inv_lref … Hl1) -Hl1 * #K1 [ #V1 | #W1 #l ] #HLK1 [ #Hl1 | #Hl #H ]
[ lapply (lstas_inv_O … H2) -H2 #H destruct // ]
elim (snv_inv_lref … H1) -H1 #I0 #K0 #X0 #HLK0 #HX0
elim (da_inv_lref … Hl1) -Hl1 * #K1 [ #V1 | #W1 #l ] #HLK1 [ #Hl1 | #Hl #H ]