2015-01-06 鳥たちの結合条件 この森の任意の鳥A,Bに対して、任意の鳥xを取れば、Cx = A(Bx)となるような鳥Cがいる。 任意の鳥A,Bに対して,AとBを結合する鳥Cが存在する。 Axiom bird_composition : forall A B : Bird, exists C : Bird, forall x : Bird, bird_respond C x = bird_respond A (bird_respond B x).日本語ってあいまいだなあと思う。