morita_non https://blog.hatena.ne.jp/morita_non/ memo https://morita-non.hatenadiary.org/ Imp_J.v プログラム正当性 (Optional) 長いうえに何やってんのか分がんね。apply with の使いかたは何となく分かった気がしないでもない。現在のコンテキストは H(仮定orなんかの定理)そのものである場合 apply H.現在のコンテキスト((サブ)ゴールにある命題)は、全称修飾のパラメータつき命題 (関数)H にあるパラメータ xを適用したものである場合は apply H with x.あるいは、 apply (H x).とも書ける。 Theorem ceval_step_more: forall i1 i2 st st' c, i1 <= i2 -> ceval_st… 190 <iframe src="https://hatenablog-parts.com/embed?url=https%3A%2F%2Fmorita-non.hatenadiary.org%2Fentry%2F20131001%2F1380631688" title=" - memo" class="embed-card embed-blogcard" scrolling="no" frameborder="0" style="display: block; width: 100%; height: 190px; max-width: 500px; margin: 10px 0px;"></iframe> Hatena Blog https://hatena.blog 2013-10-01 21:48:08 rich https://morita-non.hatenadiary.org/entry/20131001/1380631688 1.0 100%