Nuprl Lemma : per-int_wf
per-int() ∈ Type
Proof
Definitions occuring in Statement :
per-int: per-int(),
member: t ∈ T,
universe: Type
Definitions unfolded in proof :
member: t ∈ T,
uall: ∀[x:A]. B[x],
per-int: per-int(),
uand: uand(A;B),
has-value: (a)↓,
subtype_rel: A ⊆r B,
prop: ℙ,
top: Top
Lemmas referenced :
uand_wf,
has-value_wf_base,
is-exception_wf,
sqle_wf_base,
top_wf,
base_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
sqequalIntensionalEquality,
hypothesisEquality,
sqequalRule,
baseApply,
closedConclusion,
baseClosed,
hypothesis,
pertypeEquality,
equalityTransitivity,
equalitySymmetry,
applyEquality,
lambdaEquality,
divergentSqle,
sqleReflexivity,
rename,
isectEquality,
isect_memberFormation,
axiomSqleEquality,
isaxiomCases,
axiomSqEquality,
isect_memberEquality,
because_Cache,
voidElimination,
voidEquality,
promote_hyp
Latex:
per-int() \mmember{} Type
Date html generated:
2019_06_20-AM-11_29_57
Last ObjectModification:
2018_08_21-AM-00_12_49
Theory : per!type
Home
Index