---

Step * 1 of Lemma dep-isect-value-type


1. A : Type
2. B : A ⟶ Type
3. value-type(A) ∨ (∀a:A. value-type(B[a]))
4. x : Base
5. x ∈ a:A ⋂ B[a]
6. v : a:A ⋂ B[a]
⊢ 0 ≤ eval v; 0
BY
{ (DepIsectHD (-1)
   THEN Fold `has-value` 0
   THEN D 3
   THEN Try (Complete (ProveHasValue))
   THEN Thin (-1)
   THEN ProveHasValue)⋅ }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  A  {}\mrightarrow{}  Type
3.  value-type(A)  \mvee{}  (\mforall{}a:A.  value-type(B[a]))
4.  x  :  Base
5.  x  \mmember{}  a:A  \mcap{}  B[a]
6.  v  :  a:A  \mcap{}  B[a]
\mvdash{}  0  \mleq{}  eval  v;  0


By

---

Latex:
(DepIsectHD  (-1)
  THEN  Fold  `has-value`  0
  THEN  D  3
  THEN  Try  (Complete  (ProveHasValue))
  THEN  Thin  (-1)
  THEN  ProveHasValue)\mcdot{}

---

Home Index