Nuprl Lemma : bound-term_wf

[opr:Type]. (bound-term(opr) ∈ Type)


Proof




Definitions occuring in Statement :  bound-term: bound-term(opr) uall: [x:A]. B[x] member: t ∈ T universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T bound-term: bound-term(opr)
Lemmas referenced :  list_wf varname_wf term_wf istype-universe
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut sqequalRule productEquality extract_by_obid sqequalHypSubstitution isectElimination thin hypothesis hypothesisEquality axiomEquality equalityTransitivity equalitySymmetry instantiate universeEquality

Latex:
\mforall{}[opr:Type].  (bound-term(opr)  \mmember{}  Type)



Date html generated: 2020_05_19-PM-09_53_50
Last ObjectModification: 2020_03_09-PM-04_08_23

Theory : terms


Home Index