---

Step * of Lemma DVp_Pointer_wf

∀[ptr:C_LVALUE()?]. (DVp_Pointer(ptr) ∈ C_DVALUEp())
BY
{ DepprodCoDatatypeConstructorWf `C_DVALUEp_size` }

---

Latex:


\mforall{}[ptr:C\_LVALUE()?].  (DVp\_Pointer(ptr)  \mmember{}  C\_DVALUEp())


By

DepprodCoDatatypeConstructorWf  `C\_DVALUEp\_size`

---

Home Index