elim (lift_inv_flat1 … H) -H #W #U #HVW #HTU #H destruct
elim (lift_total V0 d e) #W0 #HVW0
elim (lift_total V1 d e) #W1 #HVW1
elim (lift_total T1 (d+1) e) #U1 #HTU1
@(snv_appl … a … W0 … W1 … U1 l)
elim (lift_inv_flat1 … H) -H #W #U #HVW #HTU #H destruct
elim (lift_total V0 d e) #W0 #HVW0
elim (lift_total V1 d e) #W1 #HVW1
elim (lift_total T1 (d+1) e) #U1 #HTU1
@(snv_appl … a … W0 … W1 … U1 l)