DEFINITION nf0_dec()
TYPE =
       ∀t1:T.(or ∀t2:T.(pr0 t1 t2)→(eq T t1 t2) (ex2 T λt2:T.(eq T t1 t2)→∀P:Prop.P λt2:T.pr0 t1 t2))
BODY =
Show proof