---

Step * of Lemma urec_induction

∀[F:Type ⟶ Type]
  (destructor{i:l}(T.F[T])
     ⇒ (∀[P:urec(F) ⟶ ℙ]
           ((∀[T:Type]. ((∀x:T ⋂ urec(F). P[x]) ⇒ (∀x:F T ⋂ urec(F). P[x]))) ⇒ (∀x:urec(F). P[x])))) supposing 
     ((∀T:Type. ((T ⊆r Base) ⇒ ((F T) ⊆r Base))) and 
     Monotone(T.F[T]))
BY
{ TACTIC:(Auto THEN Try (((DoSubsume THEN Auto THEN BLemma `isect2_subtype_rel`) THEN Auto))) }

1
1. [F] : Type ⟶ Type
2. Monotone(T.F[T])
3. ∀T:Type. ((T ⊆r Base) ⇒ ((F T) ⊆r Base))
4. destructor{i:l}(T.F[T])
5. [P] : urec(F) ⟶ ℙ
6. ∀[T:Type]. ((∀x:T ⋂ urec(F). P[x]) ⇒ (∀x:F T ⋂ urec(F). P[x]))
7. x : urec(F)
⊢ P[x]

---

Latex:

---

Latex:
\mforall{}[F:Type  {}\mrightarrow{}  Type]
    (destructor\{i:l\}(T.F[T])
          {}\mRightarrow{}  (\mforall{}[P:urec(F)  {}\mrightarrow{}  \mBbbP{}]
                      ((\mforall{}[T:Type].  ((\mforall{}x:T  \mcap{}  urec(F).  P[x])  {}\mRightarrow{}  (\mforall{}x:F  T  \mcap{}  urec(F).  P[x])))
                      {}\mRightarrow{}  (\mforall{}x:urec(F).  P[x]))))  supposing 
          ((\mforall{}T:Type.  ((T  \msubseteq{}r  Base)  {}\mRightarrow{}  ((F  T)  \msubseteq{}r  Base)))  and 
          Monotone(T.F[T]))


By

---

Latex:
TACTIC:(Auto  THEN  Try  (((DoSubsume  THEN  Auto  THEN  BLemma  `isect2\_subtype\_rel`)  THEN  Auto)))

---

Home Index