DEFINITION nf2_sn3()
TYPE =
∀
c:
C
.
∀
t:
T
.(
sn3
c t)
→
(
ex2
T
λ
u:
T
.
pr3
c t u
λ
u:
T
.
nf2
c u)
BODY =
Show proof