["aa","bb",f["cc","dd"]]=["aa","bb","cc","dd"]なるfが存在しないことは、
チャーチ・ロッサー性で説明できる。

チャーチ・ロッサー性は、簡単に言うと、計算の順番を変えても
最終的な計算結果が変わることが無いという性質。

もし上記のようなfがあるとすると、以下の2つの式の計算結果が同じでなければならない。
なぜなら、これら2つの式は、一番内側のfを先に計算するかどうかの違いしかないから。

null(tail(tail(tail ["aa","bb",f["cc","dd"]])))
null(tail(tail(tail ["aa","bb","cc","dd"])))

しかし、計算すればわかるが、上はtrueで下はfalseになるので矛盾する。
よってfは存在し得ない。

本当は、型なしラムダ計算に落としこんでからやる必要があるけど、
(型なしラムダ計算にチャーチ・ロッサー性があることは証明済み)
骨子としてはこんな感じ。