Li-Fan Chen
says to
YSITD
就是利用 inference rule 把欲證的 Lemma 轉出來的ㄚ