# Re: [PVS-Help] elementary prove questions

```This is a proof of lemma b in try2:

%|- b : PROOF
%|- (then (expand "a") (lemma "c") (skolem -1 "x") (inst -1 "x"))
%|- QED

Cesar

On Tue, 2005-11-15 at 14:04, Vladimir Voevodsky wrote:
> Hello,
>
> questions:
>
> 1. I am looking at the theory:
>
> try1: theory
> begin
> t:type
> a:t
> end try1
>
> When I try to typecheck I get a tcc asking me to prove that t is non-
> empty. On the other hand looking at the examples in the wift-tutorial
> (e.g. the phonebook) I got the impression that a:t would be treated
> as a declaration of a member in t and that it would imply rather than
> require that t is non-empty.
>
> 2. I am looking at the theory
>
> try2: Theory
> Begin
>    t: type
>    c: axiom exists (x: t): true
>    a: bool = (Forall (x: t): x/=x)
>    b: Theorem not a
> End try2
>
> How can I prove the theorem? If I add a line d:t then I get (as in 1)
> a tcc which I can then prove using c. After that (grind) proves the
> theorem. But I was not able to use c directly without an explicit
> line saying d:t.
>
> Thank you,