[PVS-Help] Hopefully Simple Proof Question

["Baldwin Rusty O Civ AFIT/ENGE" <Rusty.Baldwin@xxxxxxxx>]

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
 
   a_graph: simple_digraph = (# vert := add(zz, add(z, add(x,
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
    % (# vert := add(zz, add(z, add(x, singleton[T](y)))),
    %    edges := add((z, zz), singleton[pair](x, y)) #)
    % expected type  simple_digraph[T]
  % unchecked
a_graph_TCC1: OBLIGATION
  (FORALL (e: edgetype[T]):
     add[pair[T]]((z, zz), singleton[pair[T]](x, y))(e) IMPLIES
      add[T](zz, add[T](z, add[T](x, singleton[T](y))))(e`1) AND
       add[T](zz, add[T](z, add[T](x, singleton[T](y))))(e`2))
   AND
   (FORALL (e: edgetype[T]):
      add[pair[T]]((z, zz), singleton[pair[T]](x, y))(e) IMPLIES e`1 /=
e`2);