---

Step * of Lemma tagged-list-messages-wf2

∀[S,V:Type]. ∀[M:Id ⟶ Type]. ∀[s:S]. ∀[v:V]. ∀[L:(t:Id × (S ⟶ V ⟶ (M[t] List))) List].
  (tagged-list-messages(s;v;L) ∈ (t:{tg:Id| M[tg]}  × M[t]) List)
BY
{ (Auto THEN DoSubsume THEN Auto THEN BLemma `subtype_rel_list` THEN Auto) }

1
1. S : Type
2. V : Type
3. M : Id ⟶ Type
4. s : S
5. v : V
6. L : (t:Id × (S ⟶ V ⟶ (M[t] List))) List
7. tagged-list-messages(s;v;L) = tagged-list-messages(s;v;L) ∈ ((t:Id × M[t]) List)
⊢ (t:Id × M[t]) ⊆r (t:{tg:Id| M[tg]}  × M[t])

---

Latex:

---

Latex:
\mforall{}[S,V:Type].  \mforall{}[M:Id  {}\mrightarrow{}  Type].  \mforall{}[s:S].  \mforall{}[v:V].  \mforall{}[L:(t:Id  \mtimes{}  (S  {}\mrightarrow{}  V  {}\mrightarrow{}  (M[t]  List)))  List].
    (tagged-list-messages(s;v;L)  \mmember{}  (t:\{tg:Id|  M[tg]\}    \mtimes{}  M[t])  List)


By

---

Latex:
(Auto  THEN  DoSubsume  THEN  Auto  THEN  BLemma  `subtype\_rel\_list`  THEN  Auto)

---

Home Index