-| #f #I #L1 #K1 #V1 #_ #IH #X #f2 #H #f1 #Hf2 elim (after_inv_nxx … Hf2) -Hf2 [2,3: // ]
- #g2 #Hg2 #H2 destruct elim (lexs_inv_next1 … H) -H
- #L2 #V2 #HL12 #HV12 #H destruct elim (IH … HL12 … Hg2) -g2
- /3 width=3 by drops_drop, ex2_intro/
-| #f #I #L1 #K1 #V1 #W1 #HLK #HWV #IH #X #f2 #H #f1 #Hf2 elim (after_inv_pxx … Hf2) -Hf2 [1,3:* |*: // ]
- #g1 #g2 #Hg2 #H1 #H2 destruct
- [ elim (lexs_inv_push1 … H) | elim (lexs_inv_next1 … H) ] -H
- #L2 #V2 #HL12 #HV12 #H destruct elim (IH … HL12 … Hg2) -g2
- [ elim (HP … HV12 … HLK … HWV) | elim (HN … HV12 … HLK … HWV) ] -V1
- /3 width=5 by lexs_next, lexs_push, drops_skip, ex2_intro/
+| #f #I #L1 #K1 #V1 #_ #IH #Hf #f2 #X #H #f1 #Hf2
+ elim (coafter_inv_nxx … Hf2) -Hf2 [2,3: // ] #g2 #Hg2 #H2 destruct
+ elim (lexs_inv_push1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct
+ elim (IH … HL12 … Hg2) -g2
+ /3 width=3 by isuni_inv_next, drops_drop, ex2_intro/
+| #f #I #L1 #K1 #V1 #W1 #HLK #HWV #IH #Hf #f2 #X #H #f1 #Hf2
+ lapply (isuni_inv_push … Hf ??) -Hf [3: |*: // ] #Hf
+ lapply (drops_fwd_isid … HLK … Hf) -HLK #H0 destruct
+ lapply (lifts_fwd_isid … HWV … Hf) -HWV #H0 destruct
+ elim (coafter_inv_pxx … Hf2) -Hf2 [1,3:* |*: // ] #g1 #g2 #Hg2 #H1 #H2 destruct
+ [ elim (lexs_inv_push1 … H) | elim (lexs_inv_next1 … H) ] -H #L2 #V2 #HL12 #HV12 #H destruct
+ elim (IH … HL12 … Hg2) -g2 -IH /2 width=1 by isuni_isid/ #K2 #HK12 #HLK2
+ lapply (drops_fwd_isid … HLK2 … Hf) -HLK2 #H0 destruct
+ /4 width=3 by drops_refl, lexs_next, lexs_push, isid_push, ex2_intro/