Nuprl Lemma : n-tuple_wf

[n:ℕ]. (n-tuple(n) ∈ Type)


Proof




Definitions occuring in Statement :  n-tuple: n-tuple(n) nat: uall: [x:A]. B[x] member: t ∈ T universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T n-tuple: n-tuple(n) nat:
Lemmas referenced :  tuple-type_wf map_wf int_seg_wf top_wf upto_wf nat_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule lemma_by_obid sqequalHypSubstitution isectElimination thin instantiate cumulativity natural_numberEquality setElimination rename hypothesisEquality hypothesis universeEquality lambdaEquality axiomEquality equalityTransitivity equalitySymmetry

Latex:
\mforall{}[n:\mBbbN{}].  (n-tuple(n)  \mmember{}  Type)



Date html generated: 2016_05_14-PM-03_57_21
Last ObjectModification: 2015_12_26-PM-07_22_18

Theory : tuples


Home Index