---

Step * 1 of Lemma pair-list-set-type


1. T : Type
2. B : T ⟶ Type
3. L : (t:T × B[t]) List
4. L ∈ {x:t:T × B[t]| (x ∈ L)}  List
5. L = L ∈ ({x:t:T × B[t]| (x ∈ L)}  List)
⊢ {x:t:T × B[t]| (x ∈ L)}  ⊆r (t:{t:T| (t ∈ map(λp.(fst(p));L))}  × B[t])
BY
{ ((D 0 THENA Auto) THEN RepeatFor 2 (DVar `x') THEN Auto THEN MemTypeCD THEN Auto) }

1
.....set predicate..... 
1. T : Type
2. B : T ⟶ Type
3. L : (t:T × B[t]) List
4. L ∈ {x:t:T × B[t]| (x ∈ L)}  List
5. L = L ∈ ({x:t:T × B[t]| (x ∈ L)}  List)
6. t : T@i
7. x1 : B[t]@i
8. (<t, x1> ∈ L)@i
⊢ (t ∈ map(λp.(fst(p));L))

---

Latex:

---

Latex:

1.  T  :  Type
2.  B  :  T  {}\mrightarrow{}  Type
3.  L  :  (t:T  \mtimes{}  B[t])  List
4.  L  \mmember{}  \{x:t:T  \mtimes{}  B[t]|  (x  \mmember{}  L)\}    List
5.  L  =  L
\mvdash{}  \{x:t:T  \mtimes{}  B[t]|  (x  \mmember{}  L)\}    \msubseteq{}r  (t:\{t:T|  (t  \mmember{}  map(\mlambda{}p.(fst(p));L))\}    \mtimes{}  B[t])


By

---

Latex:
((D  0  THENA  Auto)  THEN  RepeatFor  2  (DVar  `x')  THEN  Auto  THEN  MemTypeCD  THEN  Auto)

---

Home Index