Specification "size.lf".

Theorem plus-exist : forall N1 N2,
  {N1: nat} => {N2:nat} => exists N3 D, {D: plus N1 N2 N3}.
induction on 1.
intros.
case H1.
apply IH to H3 H2.
exists s N3.
exists plus-s x N2 N3 D.
search.
exists N2.
exists plus-z N2. search.

Schema F := (x: nat).

Theorem ex : ctx G:F, forall N, { G |- N : nat } => false.
intros. apply plus-exist to H1 H1.