DEFINITION nf2()
TYPE =
C
→
T
→
Prop
BODY =
λ
c:
C
.
λ
t1:
T
.
∀
t2:
T
.(
pr2
c t1 t2)
→
(
eq
T
t1 t2)