Nuprl Lemma : mkinds_wf
∀[L:MutualRectypeSpec]. (mKinds ∈ Type)
Proof
Definitions occuring in Statement :
mkinds: mKinds,
mrec_spec: MutualRectypeSpec,
uall: ∀[x:A]. B[x],
member: t ∈ T,
universe: Type
Definitions unfolded in proof :
mrec_spec: MutualRectypeSpec,
uall: ∀[x:A]. B[x],
member: t ∈ T,
mkinds: mKinds,
uimplies: b supposing a,
pi1: fst(t),
prop: ℙ
Lemmas referenced :
l_member_wf,
eager-map_wf,
list_wf,
atom-value-type
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
Error :isect_memberFormation_alt,
introduction,
cut,
sqequalRule,
setEquality,
closedConclusion,
atomEquality,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
because_Cache,
hypothesisEquality,
instantiate,
productEquality,
cumulativity,
unionEquality,
universeEquality,
hypothesis,
independent_isectElimination,
Error :lambdaEquality_alt,
productElimination,
Error :productIsType,
Error :inhabitedIsType,
Error :universeIsType,
axiomEquality,
equalityTransitivity,
equalitySymmetry
Latex:
\mforall{}[L:MutualRectypeSpec]. (mKinds \mmember{} Type)
Date html generated:
2019_06_20-PM-02_14_48
Last ObjectModification:
2019_02_25-PM-01_40_55
Theory : tuples
Home
Index