あらゆる鳥はすくなくとも一羽の鳥が好き。
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.
あとから見直しても何やってるかまったく分からん!