Nuprl Lemma : corec-subtype-corec

[F,G:Type ⟶ Type].  (corec(T.F[T]) ⊆corec(T.G[T])) supposing (Monotone(T.G[T]) and (∀T:Type. (F[T] ⊆G[T])))


Definitions occuring in Statement :  corec: corec(T.F[T]) type-monotone: Monotone(T.F[T]) uimplies: supposing a subtype_rel: A ⊆B uall: [x:A]. B[x] so_apply: x[s] all: x:A. B[x] function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a so_lambda: λ2x.t[x] so_apply: x[s] all: x:A. B[x] implies:  Q subtype_rel: A ⊆B type-monotone: Monotone(T.F[T]) prop:
Lemmas referenced :  corec-subtype-corec2 subtype_rel_wf type-monotone_wf all_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin sqequalRule lambdaEquality applyEquality hypothesisEquality universeEquality independent_isectElimination lambdaFormation hypothesis dependent_functionElimination axiomEquality isect_memberEquality because_Cache equalityTransitivity equalitySymmetry instantiate cumulativity functionEquality

\mforall{}[F,G:Type  {}\mrightarrow{}  Type].
    (corec(T.F[T])  \msubseteq{}r  corec(T.G[T]))  supposing  (Monotone(T.G[T])  and  (\mforall{}T:Type.  (F[T]  \msubseteq{}r  G[T])))

Date html generated: 2016_05_14-AM-06_21_57
Last ObjectModification: 2015_12_26-PM-00_00_03

Theory : co-recursion

Home Index