[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [PVS-Help] how to prove this lemma?



Hi Bin,

A couple of uses of apply-extensionality does the trick:

(""
 (skolem * "C")
 (prop)
 (apply-extensionality :hide? t)
 (apply-extensionality 2 :hide? t))

Sam

> Hi,
> 
> Could anyone please show me how to prove the lemma "counterlemma" in the
> attached theory "standard_environments"?
> 
> Thanks a lot.
> 
> Bin