---

Step * 1 of Lemma apply_alist_wf


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

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