DEFINITION pc3()
TYPE =
C
→
T
→
T
→
Prop
BODY =
λ
c:
C
.
λ
t1:
T
.
λ
t2:
T
.
ex2
T
λ
t:
T
.
pr3
c t1 t
λ
t:
T
.
pr3
c t2 t