DEFINITION pc1()
TYPE =
       T→T→Prop
BODY =
λt1:T.λt2:T.ex2 T λt:T.pr1 t1 t λt:T.pr1 t2 t