exact ih ih_1
V_N V_T : Type
R : V_N → PE V_N V_T
xs ys : List V_T
A : V_N
n : ℕ
ih_1 : Interpretation V_N V_T R (R A, xs) (n, some ys)
ih : Interpretation V_N V_T R (R A, xs) (n, some ys) → ys.IsPrefix xs
⊢ ys.IsPrefix xs
no goals