Nuprl Lemma : test-kind_wf
∀[d:test-Obj()]. (test-kind(d) ∈ {a:Atom| (a ∈ ``prog foo prop``)} )
Proof
Definitions occuring in Statement :
test-kind: test-kind(d),
test-Obj: test-Obj(),
l_member: (x ∈ l),
cons: [a / b],
nil: [],
uall: ∀[x:A]. B[x],
member: t ∈ T,
set: {x:A| B[x]} ,
token: "$token",
atom: Atom
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
mkinds: mKinds,
cons: [a / b],
eager-map: eager-map(f;as),
list_ind: list_ind,
test-Spec: test-Spec(),
pi1: fst(t),
nil: [],
it: ⋅,
test-Obj: test-Obj(),
test-kind: test-kind(d)
Lemmas referenced :
mobj-kind_wf,
test-Spec_wf,
test-Obj_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
introduction,
cut,
sqequalRule,
sqequalHypSubstitution,
extract_by_obid,
isectElimination,
thin,
hypothesis,
hypothesisEquality,
axiomEquality,
equalityTransitivity,
equalitySymmetry,
universeIsType
Latex:
\mforall{}[d:test-Obj()]. (test-kind(d) \mmember{} \{a:Atom| (a \mmember{} ``prog foo prop``)\} )
Date html generated:
2019_10_15-AM-10_49_15
Last ObjectModification:
2019_03_25-PM-01_48_12
Theory : tree_1
Home
Index