Nuprl Lemma : is-list-if-has-value-hv-prp
∀[t:ListLike]. ((t)↓ ∈ ℙ)
Proof
Definitions occuring in Statement :
is-list-if-has-value: ListLike,
has-value: (a)↓,
uall: ∀[x:A]. B[x],
prop: ℙ,
member: t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
is-list-if-has-value: ListLike,
corec: corec(T.F[T]),
nat: ℕ,
le: A ≤ B,
and: P ∧ Q,
less_than': less_than'(a;b),
false: False,
not: ¬A,
implies: P ⇒ Q,
prop: ℙ,
all: ∀x:A. B[x],
top: Top,
uimplies: b supposing a,
unit: Unit,
so_lambda: λ2x.t[x],
so_apply: x[s]
Lemmas referenced :
false_wf,
le_wf,
primrec1_lemma,
has-value_wf-partial,
b-union_wf,
unit_wf2,
top_wf,
bunion-value-type,
equal-value-type,
product-value-type,
member_wf,
is-list-if-has-value_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
introduction,
cut,
sqequalHypSubstitution,
isectElimination,
dependent_set_memberEquality,
natural_numberEquality,
sqequalRule,
independent_pairFormation,
lambdaFormation,
hypothesis,
extract_by_obid,
thin,
hypothesisEquality,
dependent_functionElimination,
isect_memberEquality,
voidElimination,
voidEquality,
equalitySymmetry,
productEquality,
because_Cache,
independent_isectElimination,
intEquality,
lambdaEquality,
hyp_replacement,
Error :applyLambdaEquality,
instantiate,
universeEquality,
axiomEquality,
equalityTransitivity
Latex:
\mforall{}[t:ListLike]. ((t)\mdownarrow{} \mmember{} \mBbbP{})
Date html generated:
2016_10_25-AM-11_44_08
Last ObjectModification:
2016_07_12-AM-07_44_01
Theory : eval!all
Home
Index