---

Step * 2 of Lemma alist-domain-first

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

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

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

---

Latex:

---

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


By

---

Latex:
D  0

---

Home Index