assumption この tactic は忘れてもよい。仮定の中に結論と一致しているものがある場合に使うと一発で証明が終わる。でも、auto を使えば同じことができる。 intro この tactic はチュートリアルで普通に理解できる以上の機能はない。 結論が「forall x:T, U…
引用をストックしました
引用するにはまずログインしてください
引用をストックできませんでした。再度お試しください
限定公開記事のため引用できません。