DEFINITION pc1_s()
TYPE =
       ∀t2:T.∀t1:T.(pc1 t1 t2)→(pc1 t2 t1)
BODY =
Show proof