---

Step * of Lemma dseq_wf

∀[TypeNames:Type]. ∀[d:DS(TypeNames)]. ∀[a:TypeNames].
  (dseq(d;a) ∈ dstype(TypeNames; d; a) ⟶ dstype(TypeNames; d; a) ⟶ 𝔹)
BY
{ (Auto THEN D 2 THEN RepUR ``dstype dseq`` 0 THEN DoSubsume THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[TypeNames:Type].  \mforall{}[d:DS(TypeNames)].  \mforall{}[a:TypeNames].
    (dseq(d;a)  \mmember{}  dstype(TypeNames;  d;  a)  {}\mrightarrow{}  dstype(TypeNames;  d;  a)  {}\mrightarrow{}  \mBbbB{})


By

---

Latex:
(Auto  THEN  D  2  THEN  RepUR  ``dstype  dseq``  0  THEN  DoSubsume  THEN  Auto)

---

Home Index