---

Step * of Lemma iota-wf

∀[I:Cname List]. ∀[x:nameset(I)].  (iota(x) ∈ name-morph(I-[x];I))
BY
{ (Auto
   THEN D 2
   THEN (SubsumeC ⌜name-morph(I-[x];[x / I-[x]])⌝⋅ THEN Auto)
   THEN BLemma `name-morph_subtype`
   THEN Auto
   THEN BLemma `nameset_subtype`
   THEN Auto
   THEN BLemma `l_subset_cons`
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[I:Cname  List].  \mforall{}[x:nameset(I)].    (iota(x)  \mmember{}  name-morph(I-[x];I))


By

---

Latex:
(Auto
  THEN  D  2
  THEN  (SubsumeC  \mkleeneopen{}name-morph(I-[x];[x  /  I-[x]])\mkleeneclose{}\mcdot{}  THEN  Auto)
  THEN  BLemma  `name-morph\_subtype`
  THEN  Auto
  THEN  BLemma  `nameset\_subtype`
  THEN  Auto
  THEN  BLemma  `l\_subset\_cons`
  THEN  Auto)

---

Home Index