■

正しくは、こうであった。

Axiom bird_composition :
forall A B : Bird, 
exists C : Bird,
forall x : Bird,
bird_respond C x = bird_respond A (bird_respond B x).

Coqで証明出来るということから逆算した正しさに過ぎないけどな!

しかし、世の数学の偉い人らは、

「任意の鳥AとB(同じであっても異なっていてもよい)に対して、任意の鳥xをとれば、Cx = A(Bx)であるような鳥Cがいる。」

という日本語の記述で上記のような論理式をすぐさま構成出来るのか。恐しい世界だ。

そもそも今回のこれにしても、坂口和彦氏のCoqによる定理証明C83から、コンビネータの項を定義をぱくっただけだし。