DEFINITION pc1()
TYPE =
T
→
T
→
Prop
BODY =
Show proof