---

Step * 1 1 of Lemma nat-weak-overt

.....wf..... 
1. Y : Type
⊢ λA,y. lub(n.A <n, y>) ∈ Open(ℕ × Y) ⟶ Open(Y)
BY
{ TACTIC:(Unfold `Open` 0 THEN Auto) }

---

Latex:

---

Latex:
.....wf..... 
1.  Y  :  Type
\mvdash{}  \mlambda{}A,y.  lub(n.A  <n,  y>)  \mmember{}  Open(\mBbbN{}  \mtimes{}  Y)  {}\mrightarrow{}  Open(Y)


By

---

Latex:
TACTIC:(Unfold  `Open`  0  THEN  Auto)

---

Home Index