-[ #f1 #f2 #f #H elim (after_inv_O2 … H) -H /2 width=3 by ex2_intro/
-| #f1 #i1 #i2 #_ #IH * #b2 elim b2 -b2
- [ #f2 #f #H elim (after_inv_zero … H) -H
- #g #Hu #H destruct elim (IH … Hu) -f1
- /3 width=3 by at_S1, at_skip, ex2_intro/
- | -IH #b2 #IH #f2 #f #H elim (after_inv_S1 … H) -H
- #g #b #Hu #H destruct elim (IH … Hu) -f1
- /3 width=3 by at_lift, ex2_intro/
- ]
-| #f1 #b1 #i1 #i2 #_ #IH * #b2 elim b2 -b2
- [ #f2 #f #H elim (after_inv_skip … H) -H
- #g #a #Hu #H destruct elim (IH … Hu) -f1 -b1
- /3 width=3 by at_S1, at_lift, ex2_intro/
- | -IH #b2 #IH #f2 #f #H elim (after_inv_S1 … H) -H
- #g #b #Hu #H destruct elim (IH … Hu) -f1 -b1
- /3 width=3 by at_lift, ex2_intro/
- ]
+[ #f1 * #n2 #f2 * #n #f #H elim (after_inv_xOx … H) -H /2 width=3 by ex2_intro/
+| #f1 #i1 #i2 #_ #IH * #n2 #f2 * #n #f #H elim (after_inv_xOx … H) -H
+ #Hf #H destruct elim (IH … Hf) -f1 /3 width=3 by at_S1, ex2_intro/
+| #f1 #i1 #i2 #_ #IH * #n2 #f2 * #n #f #H elim (after_inv_xSx … H) -H
+ #m #Hf #Hm destruct elim (IH … Hf) -f1
+ /4 width=3 by at_plus2, at_S1, at_next, ex2_intro/