例は、forall (A B: Prop), A->(A->B)->B。これはintrosをすると、A, A->B ┣ Bとなる。これはcoqでは自動的に解決できるものであり、証明戦略的には、->除去である。 http://adam.chlipala.net/itp/tactic-reference.html によるとapplyする状況なのだが、仕…