---

Step * of Lemma urec_subtype_base

∀[F:Type ⟶ Type]. urec(F) ⊆r Base supposing ∀T:Type. ((T ⊆r Base) ⇒ ((F T) ⊆r Base))
BY
{ (Auto THEN NatInd (-1) THEN Reduce 0 THEN Try ((FHyp 2 [-1] THENA Auto)) THEN (RWW "fun_exp_add1" (-1) THEN Auto)⋅) }

---

Latex:

---

Latex:
\mforall{}[F:Type  {}\mrightarrow{}  Type].  urec(F)  \msubseteq{}r  Base  supposing  \mforall{}T:Type.  ((T  \msubseteq{}r  Base)  {}\mRightarrow{}  ((F  T)  \msubseteq{}r  Base))


By

---

Latex:
(Auto
  THEN  NatInd  (-1)
  THEN  Reduce  0
  THEN  Try  ((FHyp  2  [-1]  THENA  Auto))
  THEN  (RWW  "fun\_exp\_add1"  (-1)  THEN  Auto)\mcdot{})

---

Home Index