---

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


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

---

Latex:



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


By

Auto

---

Home Index