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