---

Step * of Lemma subset-iota_wf2

No Annotations
∀[Gamma:j⊢]. ∀[phi:{Gamma ⊢ _:𝔽}].  (iota ∈ Gamma, phi j⟶ Gamma)
BY
{ (Intros
   THEN DCubeSetMap ``context-subset`` 0
   THEN At ⌜𝕌'⌝ MemTypeCD⋅
   THEN RepUR ``subset-iota`` 0
   THEN Reduce 0
   THEN Auto
   THEN RepeatFor 2 (DVar `Gamma')
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[phi:\{Gamma  \mvdash{}  \_:\mBbbF{}\}].    (iota  \mmember{}  Gamma,  phi  j{}\mrightarrow{}  Gamma)


By

---

Latex:
(Intros
  THEN  DCubeSetMap  ``context-subset``  0
  THEN  At  \mkleeneopen{}\mBbbU{}'\mkleeneclose{}  MemTypeCD\mcdot{}
  THEN  RepUR  ``subset-iota``  0
  THEN  Reduce  0
  THEN  Auto
  THEN  RepeatFor  2  (DVar  `Gamma')
  THEN  Reduce  0
  THEN  Auto)

---

Home Index