-lemma lstas_inv_da: ∀h,g,G,L,T,U,d2. ⦃G, L⦄ ⊢ T •*[h, d2] U →
- ∃∃d1. ⦃G, L⦄ ⊢ T ▪[h, g] d1 & ⦃G, L⦄ ⊢ U ▪[h, g] d1-d2.
-#h #g #G #L #T #U #d2 #H elim H -G -L -T -U -d2
-[ #G #L #d2 #k elim (deg_total h g k) /4 width=3 by da_sort, deg_iter, ex2_intro/
+lemma lstas_inv_da: ∀h,o,G,L,T,U,d2. ⦃G, L⦄ ⊢ T •*[h, d2] U →
+ ∃∃d1. ⦃G, L⦄ ⊢ T ▪[h, o] d1 & ⦃G, L⦄ ⊢ U ▪[h, o] d1-d2.
+#h #o #G #L #T #U #d2 #H elim H -G -L -T -U -d2
+[ #G #L #d2 #s elim (deg_total h o s) /4 width=3 by da_sort, deg_iter, ex2_intro/