DEFINITION ex2_nf2()
TYPE =
       nf2 ex2_c ex2_t
BODY =
Show proof