---

Step * of Lemma list-prod-set-type

∀[A,T:Type]. ∀[L:(A × T) List]. ∀[P:T ⟶ ℙ].  L ∈ (A × {x:T| P[x]} ) List supposing (∀p∈L.P[snd(p)])
BY
{ (Auto THEN SubsumeC ⌜{p:A × T| P[snd(p)]}  List⌝⋅ THEN Auto THEN BLemma `subtype_rel_list` THEN Auto) }

1
1. A : Type
2. T : Type
3. L : (A × T) List
4. P : T ⟶ ℙ
5. (∀p∈L.P[snd(p)])
6. L = L ∈ ({p:A × T| P[snd(p)]}  List)
⊢ {p:A × T| P[snd(p)]}  ⊆r (A × {x:T| P[x]} )

---

Latex:

---

Latex:
\mforall{}[A,T:Type].  \mforall{}[L:(A  \mtimes{}  T)  List].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbP{}].    L  \mmember{}  (A  \mtimes{}  \{x:T|  P[x]\}  )  List  supposing  (\mforall{}p\mmember{}L.P[snd(p)])


By

---

Latex:
(Auto  THEN  SubsumeC  \mkleeneopen{}\{p:A  \mtimes{}  T|  P[snd(p)]\}    List\mkleeneclose{}\mcdot{}  THEN  Auto  THEN  BLemma  `subtype\_rel\_list`  THEN  Auto\000C)

---

Home Index