ptrcmd
says to
YSITD
a = b 代表有個從 a 到 b 的 path, 其中 a = b 是一個 proposition