At: apply alist property 2
1. T: Type
2. as: (Label
T) List
3. d: T
4. x: Label
5. (first a 
as s.t. (
p.1of(p) =
x)(a) else < x,d > ) = < x,d >
2of((first p as s.t. 1of(p) = x else < x,d > )) = d
By:
ReduceSOAps -1
THEN
Reduce -1
THEN
HypSubst -1 0
THEN
Reduce 0
Generated subgoals:None
About:
