【Coq】コンピューターで証明しよう【コック】©2ch.net

[0116 追加 2015/03/19(木) 15:03:19.56 ID:g9YALw9l]

ちなみに、
Proof.
intros x a.
unfold mu.
intros P b.
apply b.
apply (m mu P).
intros x0 y.
apply y.
までが上記の結果です。