@kikx さんと @lyrical_logical さんに教えてもらってます。 ichii386@count% coqtop [..ecture/functional/coq] Welcome to Coq 8.2pl2 (July 2010) Coq < Goal forall (P Q: Prop), (P -> Q) -> P -> Q. 1 subgoal ============================ forall P …