DEFINITION pr0_subst1()
TYPE =
       ∀t1:T.∀t2:T.(pr0 t1 t2)→∀v1:T.∀w1:T.∀i:nat.(subst1 i v1 t1 w1)→∀v2:T.(pr0 v1 v2)→(ex2 T λw2:T.pr0 w1 w2 λw2:T.subst1 i v2 t2 w2)
BODY =
Show proof