CCG to Lambda conversion

Premise 1: John walked .

\binom{rp \frac{\binom{ba \frac{\binom{lex \frac{\binom{\binom{John}{N}}{_john}}{NP}}{_john} \binom{\binom{walked}{S_{[dcl=true]} \NP}}{\x0._walk(x0)}}{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}}{_nobody} \binom{\binom{walked}{S_{[dcl=true]} \NP}}{\x0._walk(x0)}}{S_{[dcl=true]}}}{_walk(_nobody)} \binom{\binom{.}{}}{\X.X}}{S_{[dcl=true]}}}{_walk(_nobody)}

Script piped to coq

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

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