型検査（推論？）がうまくいってもよさそうだけどうまくいかない話です．挙動は Coq 8.5pl2 で確認しました．他のバージョンでどうかは調べていません．Set Implicit Arguments してから，なんか依存型を定義します． Coq < Set Implicit Arguments. Coq < I…