---

Step * of Lemma pair-list-set-type

∀[T:Type]. ∀[B:T ⟶ Type]. ∀[L:(t:T × B[t]) List].  (L ∈ (t:{t:T| (t ∈ map(λp.(fst(p));L))}  × B[t]) List)
BY
{ (Auto
   THEN (InstLemma `list-set-type` [⌜t:T × B[t]⌝;⌜L⌝]⋅ THENA Auto)
   THEN (DoSubsume THEN Auto THEN SubtypeReasoning1 THEN Auto)⋅) }

1
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])

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[B:T  {}\mrightarrow{}  Type].  \mforall{}[L:(t:T  \mtimes{}  B[t])  List].    (L  \mmember{}  (t:\{t:T|  (t  \mmember{}  map(\mlambda{}p.(fst(p));L))\}    \mtimes{}  B[t])\000C  List)


By

---

Latex:
(Auto
  THEN  (InstLemma  `list-set-type`  [\mkleeneopen{}t:T  \mtimes{}  B[t]\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (DoSubsume  THEN  Auto  THEN  SubtypeReasoning1  THEN  Auto)\mcdot{})

---

Home Index