Nuprl Lemma : stream_subtype_base
∀[T:Type]. stream(T) ⊆r Base supposing T ⊆r Base
Proof
Definitions occuring in Statement :
stream: stream(A),
uimplies: b supposing a,
subtype_rel: A ⊆r B,
uall: ∀[x:A]. B[x],
base: Base,
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
uimplies: b supposing a,
stream: stream(A),
so_lambda: λ2x.t[x],
so_apply: x[s],
all: ∀x:A. B[x],
implies: P ⇒ Q,
prop: ℙ,
subtype_rel: A ⊆r B
Lemmas referenced :
corec_subtype_base,
sqn+1type_product,
sqntype_subtype_base,
sqntype_wf,
nat_wf,
subtype_rel_wf,
base_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
introduction,
cut,
sqequalRule,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
lambdaEquality,
productEquality,
hypothesisEquality,
universeEquality,
independent_isectElimination,
lambdaFormation,
hypothesis,
axiomEquality,
isect_memberEquality,
because_Cache,
equalityTransitivity,
equalitySymmetry
Latex:
\mforall{}[T:Type]. stream(T) \msubseteq{}r Base supposing T \msubseteq{}r Base
Date html generated:
2019_06_20-PM-00_37_39
Last ObjectModification:
2018_08_17-PM-04_32_22
Theory : co-recursion
Home
Index