DEFINITION nf2_dec()
TYPE =
       ∀c:C.∀t1:T.(or (nf2 c t1) (ex2 T λt2:T.(eq T t1 t2)→∀P:Prop.P λt2:T.pr2 c t1 t2))
BODY =
Show proof