---

Step * 1 of Lemma dl-obj-prog_wf


1. x : dl-Obj()
2. dl-kind(x) = "prog" ∈ Atom
⊢ dl-obj-prog(x) ∈ Prog
BY
{ (D 1 THEN RepUR ``dl-kind mobj-kind`` -1 THEN HypSubst' (-1) (-2) THEN Unfold `dl-obj-prog` 0 THEN Reduce 0) }

1
1. i : mKinds
2. x1 : mtype(dl-Spec();"prog")
3. i = "prog" ∈ Atom
⊢ x1 ∈ Prog

---

Latex:

---

Latex:

1.  x  :  dl-Obj()
2.  dl-kind(x)  =  "prog"
\mvdash{}  dl-obj-prog(x)  \mmember{}  Prog


By

---

Latex:
(D  1
  THEN  RepUR  ``dl-kind  mobj-kind``  -1
  THEN  HypSubst'  (-1)  (-2)
  THEN  Unfold  `dl-obj-prog`  0
  THEN  Reduce  0)

---

Home Index