CCG to Lambda conversion

Premise 1: John walked .

\binom{rp \frac{\binom{ba \frac{\binom{lex \frac{\binom{\binom{John}{N}}{_john}}{NP}}{\F.F(_john)} \binom{\binom{walked}{S_{[dcl=true]} \NP}}{\Q.Q(\x._walk(x))}}{S_{[dcl=true]}}}{_walk(_john)} \binom{\binom{.}{}}{\X.X}}{S_{[dcl=true]}}}{_walk(_john)}

Conclusion: Nobody walked .

\binom{rp \frac{\binom{ba \frac{\binom{\binom{Nobody}{NP}}{\P.-exists x.P(x)} \binom{\binom{walked}{S_{[dcl=true]} \NP}}{\Q.Q(\x._walk(x))}}{S_{[dcl=true]}}}{-exists x._walk(x)} \binom{\binom{.}{}}{\X.X}}{S_{[dcl=true]}}}{-exists x._walk(x)}

Script piped to coq

echo "Require Export coqlib.
Parameter _john : Entity.
Parameter _walk : Entity -> Prop.
Theorem t1: (_walk _john) -> (not (exists x, (_walk x))). Set Firstorder Depth 1. nltac. Set Firstorder Depth 6. nltac. Qed." | coqtop

echo "Require Export coqlib.
Parameter _john : Entity.
Parameter _walk : Entity -> Prop.
Theorem t1: (_walk _john) -> (not (not (exists x, (_walk x)))). Set Firstorder Depth 1. nltac. Set Firstorder Depth 6. nltac. Qed." | coqtop