---

Step * 1 1 of Lemma urec_subtype


1. F : Type ⟶ Type
⊢ urec(F) ⊆r ⋃n:ℕ.(F (F^n Void))
BY
{ TACTIC:((D 0 THEN Auto) THEN Unfold `urec` (-1)) }

1
1. F : Type ⟶ Type
2. x : ⋃n:ℕ.(F^n Void)
⊢ x ∈ ⋃n:ℕ.(F (F^n Void))

---

Latex:

---

Latex:

1.  F  :  Type  {}\mrightarrow{}  Type
\mvdash{}  urec(F)  \msubseteq{}r  \mcup{}n:\mBbbN{}.(F  (F\^{}n  Void))


By

---

Latex:
TACTIC:((D  0  THEN  Auto)  THEN  Unfold  `urec`  (-1))

---

Home Index