Step
*
of Lemma
DVp_Null_wf
∀[x:Unit]. (DVp_Null(x) ∈ C_DVALUEp())
BY
{ DepprodCoDatatypeConstructorWf `C_DVALUEp_size` }
Latex:
\mforall{}[x:Unit].  (DVp\_Null(x)  \mmember{}  C\_DVALUEp())
By
DepprodCoDatatypeConstructorWf  `C\_DVALUEp\_size`
Home
Index