Nuprl Lemma : partial-term-0-subset

[H,xx,u:Top].  (partial-term-0(H, xx;u) partial-term-0(H;u))


Proof




Definitions occuring in Statement :  partial-term-0: u[0] context-subset: Gamma, phi uall: [x:A]. B[x] top: Top sqequal: t
Definitions unfolded in proof :  member: t ∈ T uall: [x:A]. B[x] csm-id: 1(X) csm-id-adjoin: [u] partial-term-0: u[0]
Lemmas referenced :  top_wf
Rules used in proof :  because_Cache hypothesisEquality thin isectElimination isect_memberEquality sqequalHypSubstitution hypothesis lemma_by_obid sqequalAxiom cut introduction isect_memberFormation computationStep sqequalTransitivity sqequalReflexivity sqequalRule sqequalSubstitution

Latex:
\mforall{}[H,xx,u:Top].    (partial-term-0(H,  xx;u)  \msim{}  partial-term-0(H;u))



Date html generated: 2016_05_19-AM-08_40_17
Last ObjectModification: 2016_04_13-AM-11_12_36

Theory : cubical!type!theory


Home Index