[PVS-Help] Hopefully Simple Proof Question

```Hello,

I have what I hope is a simple question to help me dispatch a type check
obligation.  Below is a pvs file that generates the tc OBLIGATION that
follows it.

I THINK what the obligation is telling me is that for all edges e I add,
e`1 and e`2 are vertices in the graph AND e`1 /= e`2.

I'm not sure how to prove the first part (e`1 and e`2 are vertices) and
I tried to use the commented out type TT to handle the second part
(which it didn't).

Thanks for any insight.

Rusty

===========
jj [ T: TYPE+ ]
: THEORY

BEGIN

%   TT: TYPE+ = {a,b:T | a /= b}

IMPORTING digraphs@digraphs[T]

x, y, z, zz: T

singleton[T](y)))), edges := add((z,zz), singleton[pair](x,y)) #)

edge_test: THEOREM edge?(a_graph)(x,y) AND edge?(a_graph)(z,zz)

End jj
============
% Subtype TCC generated (at line 12, column 29) for
%    edges := add((z, zz), singleton[pair](x, y)) #)
% expected type  simple_digraph[T]
% unchecked
a_graph_TCC1: OBLIGATION
(FORALL (e: edgetype[T]):