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