---

Step * 1 1 of Lemma fpf-as-apply-alist


1. A : Type
2. B : Type
3. d : A List
4. f1 : a:{a:A| (a ∈ d)}  ⟶ B
5. eq : EqDecider(A)
6. map(λx.<x, f1 x>;d) ∈ (A × B) List
7. x : A
8. (x ∈ d)
9. ∀[i:ℕ||map(λx.<x, f1 x>;d)||]
     (apply-alist(eq;map(λx.<x, f1 x>;d);x) ~ inl (snd(map(λx.<x, f1 x>;d)[i]))) supposing 
        (((fst(map(λx.<x, f1 x>;d)[i])) = x ∈ A) and 
        (∀j:ℕi. (¬((fst(map(λx.<x, f1 x>;d)[j])) = x ∈ A))))
⊢ (f1 x) = outl(apply-alist(eq;map(λx.<x, f1 x>;d);x)) ∈ B
BY
{ xxxAssert ⌜∃i:ℕ||d||. ((∀j:ℕi. (¬((fst(map(λx.<x, f1 x>;d)[j])) = x ∈ A))) ∧ ((fst(map(λx.<x, f1 x>;d)[i])) = x ∈ A))⌝
⋅xxx }

1
.....assertion..... 
1. A : Type
2. B : Type
3. d : A List
4. f1 : a:{a:A| (a ∈ d)}  ⟶ B
5. eq : EqDecider(A)
6. map(λx.<x, f1 x>;d) ∈ (A × B) List
7. x : A
8. (x ∈ d)
9. ∀[i:ℕ||map(λx.<x, f1 x>;d)||]
     (apply-alist(eq;map(λx.<x, f1 x>;d);x) ~ inl (snd(map(λx.<x, f1 x>;d)[i]))) supposing 
        (((fst(map(λx.<x, f1 x>;d)[i])) = x ∈ A) and 
        (∀j:ℕi. (¬((fst(map(λx.<x, f1 x>;d)[j])) = x ∈ A))))
⊢ ∃i:ℕ||d||. ((∀j:ℕi. (¬((fst(map(λx.<x, f1 x>;d)[j])) = x ∈ A))) ∧ ((fst(map(λx.<x, f1 x>;d)[i])) = x ∈ A))

2
1. A : Type
2. B : Type
3. d : A List
4. f1 : a:{a:A| (a ∈ d)}  ⟶ B
5. eq : EqDecider(A)
6. map(λx.<x, f1 x>;d) ∈ (A × B) List
7. x : A
8. (x ∈ d)
9. ∀[i:ℕ||map(λx.<x, f1 x>;d)||]
     (apply-alist(eq;map(λx.<x, f1 x>;d);x) ~ inl (snd(map(λx.<x, f1 x>;d)[i]))) supposing 
        (((fst(map(λx.<x, f1 x>;d)[i])) = x ∈ A) and 
        (∀j:ℕi. (¬((fst(map(λx.<x, f1 x>;d)[j])) = x ∈ A))))
10. ∃i:ℕ||d||. ((∀j:ℕi. (¬((fst(map(λx.<x, f1 x>;d)[j])) = x ∈ A))) ∧ ((fst(map(λx.<x, f1 x>;d)[i])) = x ∈ A))
⊢ (f1 x) = outl(apply-alist(eq;map(λx.<x, f1 x>;d);x)) ∈ B

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  d  :  A  List
4.  f1  :  a:\{a:A|  (a  \mmember{}  d)\}    {}\mrightarrow{}  B
5.  eq  :  EqDecider(A)
6.  map(\mlambda{}x.<x,  f1  x>d)  \mmember{}  (A  \mtimes{}  B)  List
7.  x  :  A
8.  (x  \mmember{}  d)
9.  \mforall{}[i:\mBbbN{}||map(\mlambda{}x.<x,  f1  x>d)||]
          (apply-alist(eq;map(\mlambda{}x.<x,  f1  x>d);x)  \msim{}  inl  (snd(map(\mlambda{}x.<x,  f1  x>d)[i])))  supposing 
                (((fst(map(\mlambda{}x.<x,  f1  x>d)[i]))  =  x)  and 
                (\mforall{}j:\mBbbN{}i.  (\mneg{}((fst(map(\mlambda{}x.<x,  f1  x>d)[j]))  =  x))))
\mvdash{}  (f1  x)  =  outl(apply-alist(eq;map(\mlambda{}x.<x,  f1  x>d);x))


By

---

Latex:
xxxAssert  \mkleeneopen{}\mexists{}i:\mBbbN{}||d||
                        ((\mforall{}j:\mBbbN{}i.  (\mneg{}((fst(map(\mlambda{}x.<x,  f1  x>d)[j]))  =  x)))  \mwedge{}  ((fst(map(\mlambda{}x.<x,  f1  x>d)[i]))  =  x))\mkleeneclose{}
\mcdot{}xxx

---

Home Index