Li-Fan Chen
says to
YSITD
從 lambda 借用概念就是 alpha-equivalence