Imp_J.v プログラム正当性 (Optional) 長いうえに何やってんのか分がんね。apply with の使いかたは何となく分かった気がしないでもない。現在のコンテキストは H(仮定orなんかの定理)そのものである場合 apply H.現在のコンテキスト((サブ)ゴールにある命題…
引用をストックしました
引用するにはまずログインしてください
引用をストックできませんでした。再度お試しください
限定公開記事のため引用できません。