-fact liftsv_inv_cons1_aux: ∀f:rtmap. ∀X,Y. ⬆*[f] X ≘ Y →
- ∀T1,T1s. X = T1 ⨮ T1s →
- ∃∃T2,T2s. ⬆*[f] T1 ≘ T2 & ⬆*[f] T1s ≘ T2s &
- Y = T2 ⨮ T2s.
+fact liftsv_inv_cons1_aux (f):
+ ∀X,Y. ⇧*[f] X ≘ Y → ∀T1,T1s. X = T1 ⨮ T1s →
+ ∃∃T2,T2s. ⇧*[f] T1 ≘ T2 & ⇧*[f] T1s ≘ T2s & Y = T2 ⨮ T2s.