Nuprl Lemma : per-value_subtype_base
per-value() ⊆r Base
Proof
Definitions occuring in Statement :
per-value: per-value(),
subtype_rel: A ⊆r B,
base: Base
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
so_lambda: λ2x.t[x],
prop: ℙ,
so_apply: x[s],
per-value: per-value()
Lemmas referenced :
subtype_rel-per-set,
base_wf,
has-value_wf_base
Rules used in proof :
cut,
lemma_by_obid,
sqequalHypSubstitution,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isectElimination,
thin,
hypothesis,
sqequalRule,
lambdaEquality,
hypothesisEquality
Latex:
per-value() \msubseteq{}r Base
Date html generated:
2016_05_13-PM-03_54_35
Last ObjectModification:
2015_12_26-AM-10_40_36
Theory : per!type
Home
Index