---

Step * of Lemma dl-obj-prop_wf

∀[x:dl-Obj()]. dl-obj-prop(x) ∈ Prop supposing dl-kind(x) = "prop" ∈ Atom
BY
{ (Intros
   THEN Unhide
   THEN D 1
   THEN RepUR ``dl-kind mobj-kind`` -1
   THEN HypSubst' (-1) (-2)
   THEN Unfold `dl-obj-prop` 0
   THEN Reduce 0
   THEN InferEqualType
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Intros
  THEN  Unhide
  THEN  D  1
  THEN  RepUR  ``dl-kind  mobj-kind``  -1
  THEN  HypSubst'  (-1)  (-2)
  THEN  Unfold  `dl-obj-prop`  0
  THEN  Reduce  0
  THEN  InferEqualType
  THEN  Auto)

---

Home Index