Inductive t:Set := c: (t -> nat) -> t.