Step * 1 of Lemma apply_alist_wf


1. Type
2. eq EqDecider(T)
3. T
4. Type
5. u1 T
6. u2 V
7. (T × V) List
8. apply_alist(eq;v;x) ∈ {v@0:V| (<x, v@0> ∈ v)}  supposing (x ∈ map(λa.(fst(a));v))
9. u1 ∈ T
10. Unit
11. eq u1 inr 
12. uiff(u1 x ∈ T;↑(inr ))
⊢ apply_alist(eq;v;x) ∈ {v@0:V| (<x, v@0> ∈ [<u1, u2> v])} 
BY
(D -1 THEN -2 THEN Auto) }

1
1. Type
2. eq EqDecider(T)
3. T
4. Type
5. u1 T
6. u2 V
7. (T × V) List
8. apply_alist(eq;v;x) ∈ {v@0:V| (<x, v@0> ∈ v)}  supposing (x ∈ map(λa.(fst(a));v))
9. u1 ∈ T
10. Unit
11. eq u1 inr 
12. ↑(inr )
13. u1 x ∈ T
⊢ apply_alist(eq;v;x) ∈ {v@0:V| (<x, v@0> ∈ [<u1, u2> v])} 


Latex:


Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  x  :  T
4.  V  :  Type
5.  u1  :  T
6.  u2  :  V
7.  v  :  (T  \mtimes{}  V)  List
8.  apply\_alist(eq;v;x)  \mmember{}  \{v@0:V|  (<x,  v@0>  \mmember{}  v)\}    supposing  (x  \mmember{}  map(\mlambda{}a.(fst(a));v))
9.  x  =  u1
10.  y  :  Unit
11.  eq  u1  x  =  inr  y 
12.  uiff(u1  =  x;\muparrow{}(inr  y  ))
\mvdash{}  apply\_alist(eq;v;x)  \mmember{}  \{v@0:V|  (<x,  v@0>  \mmember{}  [<u1,  u2>  /  v])\} 


By


Latex:
(D  -1  THEN  D  -2  THEN  Auto)




Home Index