あらゆる鳥はすくなくとも一羽の鳥が好き。

Aに向ってBと呼びかければ、Aは同じ鳥Bの名を呼びもどすかもしれない。
その場合、鳥Aは鳥Bが好きであるという。
記号だと、AB = B

あらゆる鳥はすくなくとも一羽の鳥が好き。coqで。

Theorem any_bird_is_fond_of_least_one_bird :
forall A, exists B, B = bird_respond A B.

証明。

Proof.
intros.
destruct there_is_mockingbird as [M].
assert(HC: exists C, forall x, bird_respond C x = bird_respond A (bird_respond M x)).
apply bird_composition.
destruct HC as [C].
assert(HCC: bird_respond C C = bird_respond A (bird_respond M C)).
apply H0.
exists (bird_respond C C).
assert(HM : bird_respond C C = bird_respond M C).
apply H. rewrite <- HM in HCC. assumption.
Qed.

あとから見直しても何やってるかまったく分からん!