Coq での定義、具体的には CHI を使用した定義で問題が発生しています。基本的な原則については理解できましたが、これを定義しようとすると」
((A -> (A -> C)) * ((A -> C) -> A)) -> C :=
それが私に言い続けているという事実のために、私はどこにも行きません:
"Error: The type of this term is a product while it is expected to be "C"。
以前のスクリプトで使用した通常の戦術を既に試しましたが、これは同じ方法 (楽しい) を使用して解決する必要があると確信していますが、試みているように見えるすべてがそのエラーメッセージで終わります。任意のヒント？