DEFINITION sn3_nf2()
TYPE =
∀
c:
C
.
∀
t:
T
.(
nf2
c t)
→
(
sn3
c t)
BODY =
Show proof