At: apply alist member2 2 1 1
1. T: Type
2. as: (Label
T) List
3. u: LabelT
4. v: (LabelT) List
5. 
d1,d2:T, x:Label. (x 
map(
p.1of(p);v)) 
apply_alist(v;x;d1) = apply_alist(v;x;d2)
6. d1: T
7. d2: T
8. x: Label
9. x = 1of(u)
10. 
1of(u) =
x
(x map(p.1of(p);v))
By:
Analyze -1
THEN
HypSubstSq -1 0
THEN
EqLblReflexive 0
Generated subgoals:None
About:
