omega
V_N V_T : Type
R : V_N → PE V_N V_T
xs ys : List V_T
e1 e2 : PE V_N V_T
n1 n2 : ℕ
ih_1 : Interpretation V_N V_T R (e1, xs) (n1, none)
ih : ∀ m < n1 + n2 + 1, ∀ (e : PE V_N V_T), Interpretation V_N V_T R (e, xs) (m, some ys) → ys.IsPrefix xs
ih_2 : Interpretation V_N V_T R (e2, xs) (n2, some ys)
⊢ n2 < n1 + n2 + 1
no goals