P18に掲載されているものをCoqで。
http://gist.github.com/963772
Pab Pba
----------------------------- split.
forall x, exists y,Pxy Pab & Pba
---------------------- -------------------- exists y.
exists y,Pay. exists y,(Pay & Pya).
------------------------------------------------------------- intros y Pxy'.
forall y,Pay -> exists y, (Pay & Pya)
------------------------------------------------------------- elim (Pxy x).
exists y,(Pay & Pya).
--------------------------------------- intros x.
forall x, exists y, (Pxy & Pyx).はじめの数段の証明木はこんな感じか。細部が書籍と違っていたようだ。
