---

Step * of Lemma es-decl-set-declares-tag_wf

∀[dd:DeclSet]. ∀[x:Id]. ∀[T:Type].  (es-decl-set-declares-tag{i:l}(dd;x;T) ∈ ℙ')
BY
{ ((D 0 THENA Auto)
   THEN RepeatFor 2 (D -1)
   THEN RepUR ``es-decl-set-declares-tag`` 0
   THEN Auto
   THEN DoSubsume
   THEN Auto)⋅ }

---

Latex:

---

Latex:
\mforall{}[dd:DeclSet].  \mforall{}[x:Id].  \mforall{}[T:Type].    (es-decl-set-declares-tag\{i:l\}(dd;x;T)  \mmember{}  \mBbbP{}')


By

---

Latex:
((D  0  THENA  Auto)
  THEN  RepeatFor  2  (D  -1)
  THEN  RepUR  ``es-decl-set-declares-tag``  0
  THEN  Auto
  THEN  DoSubsume
  THEN  Auto)\mcdot{}

---

Home Index