-fact shnv_inv_cast_aux: ∀h,g,G,L,X,l1. ⦃G, L⦄ ⊢ X ¡[h, g, l1] → ∀U,T. X = ⓝU.T →
- ∧∧ ⦃G, L⦄ ⊢ U ¡[h, g] & ⦃G, L⦄ ⊢ T ¡[h, g]
- & (∀l2. l2 ≤ l1 → ⦃G, L⦄ ⊢ U •*⬌*[h, g, l2, l2+1] T).
-#h #g #G #L #X #l1 * -X
+fact shnv_inv_cast_aux: ∀h,o,G,L,X,d1. ⦃G, L⦄ ⊢ X ¡[h, o, d1] → ∀U,T. X = ⓝU.T →
+ ∧∧ ⦃G, L⦄ ⊢ U ¡[h, o] & ⦃G, L⦄ ⊢ T ¡[h, o]
+ & (∀d2. d2 ≤ d1 → ⦃G, L⦄ ⊢ U •*⬌*[h, o, d2, d2+1] T).
+#h #o #G #L #X #d1 * -X