DEFINITION pc1_refl()
TYPE =
       ∀t:T.(pc1 t t)
BODY =
Show proof