At:
adjl-edge-accum-properties
1
1.
A: AdjList
2.
T: Type
3.
s: T
4.
x: 
A.size
5.
f: T
A.sizeT
6.
y: A.size
7.
e: x:A.size
||A.out(x)||
8.
< 1of(e),(A.out(1of(e)))[2of(e)] > = < x,y >
(y 
A.out(x))
By:
SplitPair -1
THEN
Unfold `l_member` 0
THEN
InstConcl [2of(e)]
THEN
SubstFor x 0
Generated subgoals:
None
About:
