DEFINITION nfs2()
TYPE =
C
→
TList
→
Prop
BODY =
Show proof