Nuprl Lemma : awf-subtype
∀[T:Type]. ∀[s:awf(T)]. (s ∈ T + (awf(T) List))
Proof
Definitions occuring in Statement :
awf: awf(T),
list: T List,
uall: ∀[x:A]. B[x],
member: t ∈ T,
union: left + right,
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
awf: awf(T),
so_lambda: λ2x.t[x],
so_apply: x[s],
uimplies: b supposing a,
all: ∀x:A. B[x],
implies: P ⇒ Q,
subtype_rel: A ⊆r B,
guard: {T}
Lemmas referenced :
corec-ext,
list_wf,
continuous-monotone-union,
continuous-monotone-constant,
continuous-monotone-list,
continuous-monotone-id,
subtype_rel_weakening,
corec_wf,
awf_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
introduction,
cut,
sqequalHypSubstitution,
lemma_by_obid,
isectElimination,
thin,
sqequalRule,
lambdaEquality,
unionEquality,
hypothesisEquality,
hypothesis,
universeEquality,
independent_isectElimination,
dependent_functionElimination,
independent_functionElimination,
applyEquality,
axiomEquality,
equalityTransitivity,
equalitySymmetry,
isect_memberEquality,
because_Cache
Latex:
\mforall{}[T:Type]. \mforall{}[s:awf(T)]. (s \mmember{} T + (awf(T) List))
Date html generated:
2016_05_15-PM-07_24_26
Last ObjectModification:
2015_12_27-AM-11_24_36
Theory : general
Home
Index