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

[0121 １３２人目の素数さん 2015/04/17(金) 21:21:52.45 ID:oyQOgKjs]

>>116
Proof.
intros x a.
unfold mu.
intros P b.
apply b.
apply (m mu P).
intros x0 y.
apply y.
intro y0.
apply (b y0).
apply a.
Qed.