先生もたびたび取り違える

計算モデル論では関数型言語FLにおける型の規則。FLの記述は、関数の抽象や適用といった部分でラムダ式がそのまま出てきます。型検査と型推論のうち型検査を、FLの規則による証明という形で実行しました。しかしFLの記述はわかりにくくて紛らわしい! ':'が一つと二つでは全然意味が違うんだから(一つなら変数の型を、二つならリスト構造をあらわす)。
あと、case文の意味がよくわかってない。