Step * 1 1 1 3 1 1 1 of Lemma hdf-union_wf


1. Type@i'
⊢ ∀v@0:v. (valueall-type(v)  has-valueall(v@0))
BY
Auto }


Latex:


Latex:

1.  v  :  Type@i'
\mvdash{}  \mforall{}v@0:v.  (valueall-type(v)  {}\mRightarrow{}  has-valueall(v@0))


By


Latex:
Auto




Home Index