Nuprl Lemma : dp-vec_wf

[d:DualPlanePrimitives]. (Vec ∈ Type)


Proof




Definitions occuring in Statement :  dp-vec: Vec dual-plane-primitives: DualPlanePrimitives uall: [x:A]. B[x] member: t ∈ T universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T dual-plane-primitives: DualPlanePrimitives record+: record+ record-select: r.x subtype_rel: A ⊆B eq_atom: =a y ifthenelse: if then else fi  btrue: tt guard: {T} prop: dp-vec: Vec
Lemmas referenced :  subtype_rel_self subtype_rel_universe1 dual-plane-primitives_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut sqequalHypSubstitution dependentIntersectionElimination sqequalRule dependentIntersectionEqElimination thin hypothesis applyEquality tokenEquality instantiate extract_by_obid isectElimination universeEquality functionEquality equalityTransitivity equalitySymmetry because_Cache closedConclusion axiomEquality universeIsType

Latex:
\mforall{}[d:DualPlanePrimitives].  (Vec  \mmember{}  Type)



Date html generated: 2019_10_16-AM-11_29_17
Last ObjectModification: 2018_10_16-AM-10_36_26

Theory : matrices


Home Index