---

Step * of Lemma dl-obj-prog_wf

∀[x:dl-Obj()]. dl-obj-prog(x) ∈ Prog supposing dl-kind(x) = "prog" ∈ Atom
BY
{ (Intros THEN Unhide) }

1
1. x : dl-Obj()
2. dl-kind(x) = "prog" ∈ Atom
⊢ dl-obj-prog(x) ∈ Prog

---

Latex:

---

Latex:
\mforall{}[x:dl-Obj()].  dl-obj-prog(x)  \mmember{}  Prog  supposing  dl-kind(x)  =  "prog"


By

---

Latex:
(Intros  THEN  Unhide)

---

Home Index