---

Step * of Lemma urec-level-property

∀[F:Type ⟶ Type]
  (∀[f:destructor{i:l}(T.F[T])]. ∀[x:urec(F)].  (x ∈ F^urec-level(f;x) Void)) supposing 
     ((∀T:Type. ((T ⊆r Base) ⇒ (F[T] ⊆r Base))) and 
     Monotone(T.F[T]))
BY
{ TACTIC:((UnivCD THENA Auto) THEN Assert ⌜∀n:ℕ. ∀x:urec(F).  (urec-level(f;x) < n ⇒ (x ∈ F^urec-level(f;x) Void))⌝⋅) }

1
.....assertion..... 
1. F : Type ⟶ Type
2. Monotone(T.F[T])
3. ∀T:Type. ((T ⊆r Base) ⇒ (F[T] ⊆r Base))
4. f : destructor{i:l}(T.F[T])
5. x : urec(F)
⊢ ∀n:ℕ. ∀x:urec(F).  (urec-level(f;x) < n ⇒ (x ∈ F^urec-level(f;x) Void))

2
1. F : Type ⟶ Type
2. Monotone(T.F[T])
3. ∀T:Type. ((T ⊆r Base) ⇒ (F[T] ⊆r Base))
4. f : destructor{i:l}(T.F[T])
5. x : urec(F)
6. ∀n:ℕ. ∀x:urec(F).  (urec-level(f;x) < n ⇒ (x ∈ F^urec-level(f;x) Void))
⊢ x ∈ F^urec-level(f;x) Void

---

Latex:

---

Latex:
\mforall{}[F:Type  {}\mrightarrow{}  Type]
    (\mforall{}[f:destructor\{i:l\}(T.F[T])].  \mforall{}[x:urec(F)].    (x  \mmember{}  F\^{}urec-level(f;x)  Void))  supposing 
          ((\mforall{}T:Type.  ((T  \msubseteq{}r  Base)  {}\mRightarrow{}  (F[T]  \msubseteq{}r  Base)))  and 
          Monotone(T.F[T]))


By

---

Latex:
TACTIC:((UnivCD  THENA  Auto)
                THEN  Assert  \mkleeneopen{}\mforall{}n:\mBbbN{}.  \mforall{}x:urec(F).    (urec-level(f;x)  <  n  {}\mRightarrow{}  (x  \mmember{}  F\^{}urec-level(f;x)  Void))\mkleeneclose{}\mcdot{}
                )

---

Home Index