- | ∃∃T. ⦃G, L.ⓓV1⦄ ⊢ T1 ➡[n, h] T & ⬆*[1] U2 ≘ T & p = true.
-#n #h #p #G #L #V1 #T1 #U2 * #c #Hc #H elim (cpg_inv_abbr1 … H) -H *
-[ #cV #cT #V2 #T2 #HV12 #HT12 #H1 #H2 destruct
- elim (isrt_inv_max … Hc) -Hc #nV #nT #HcV #HcT #H destruct
- elim (isrt_inv_shift … HcV) -HcV #HcV #H destruct
- /4 width=5 by ex3_2_intro, ex2_intro, or_introl/
-| #cT #T2 #HT12 #HUT2 #H1 #H2 destruct
- /5 width=3 by isrt_inv_plus_O_dx, ex3_intro, ex2_intro, or_intror/
+ | ∃∃T. ⬆*[1] T ≘ T1 & ⦃G, L⦄ ⊢ T ➡[n, h] U2 & p = true.
+#n #h #p #G #L #V1 #T1 #U2 #H
+elim (cpm_inv_bind1 … H) -H
+[ /3 width=1 by or_introl/
+| * /3 width=3 by ex3_intro, or_intror/