【Coq】コンピューターで証明しよう【コック】©2ch.net

[0126 115 2015/04/18(土) 16:08:27.46 ID:Ch74qrhJ]

>>121
レス大感謝です。しかし、
apply (b y0).
のところで、
Error: Impossible to unify "B P y0 -> P y0" with
"B (fun x0 : A => P x0) y0 -> P y0".
と叱られました。Coqのバージョンが
Welcome to Coq 8.3pl3
で古いのでしょうか。