---

Step * 1 1 of Lemma alist-domain-first


1. [A] : Type
2. d : A List@i
3. f1 : a:{a:A| (a ∈ d)}  ─→ Top@i
4. x : A@i
5. eq : EqDecider(A)@i
6. (x ∈ d)@i
7. i : ℕ||d||
8. d[i] = x ∈ A
9. ∀j:ℕi. (¬(d[j] = x ∈ A))
⊢ ∀j:ℕi. (¬((fst(map(λx.<x, f1 x>;d)[j])) = x ∈ A))
BY
{ ParallelLast }

1
1. [A] : Type
2. d : A List@i
3. f1 : a:{a:A| (a ∈ d)}  ─→ Top@i
4. x : A@i
5. eq : EqDecider(A)@i
6. (x ∈ d)@i
7. i : ℕ||d||
8. d[i] = x ∈ A
9. ∀j:ℕi. (¬(d[j] = x ∈ A))
10. j : ℕi@i
11. ¬(d[j] = x ∈ A)
⊢ ¬((fst(map(λx.<x, f1 x>;d)[j])) = x ∈ A)

---

Latex:



1.  [A]  :  Type
2.  d  :  A  List@i
3.  f1  :  a:\{a:A|  (a  \mmember{}  d)\}    {}\mrightarrow{}  Top@i
4.  x  :  A@i
5.  eq  :  EqDecider(A)@i
6.  (x  \mmember{}  d)@i
7.  i  :  \mBbbN{}||d||
8.  d[i]  =  x
9.  \mforall{}j:\mBbbN{}i.  (\mneg{}(d[j]  =  x))
\mvdash{}  \mforall{}j:\mBbbN{}i.  (\mneg{}((fst(map(\mlambda{}x.<x,  f1  x>d)[j]))  =  x))


By

ParallelLast

---

Home Index