Nuprl Lemma : partial-term-1-subset
∀[H,xx,u:Top]. (partial-term-1(H, xx;u) ~ partial-term-1(H;u))
Proof
Definitions occuring in Statement :
partial-term-1: u[1],
context-subset: Gamma, phi,
uall: ∀[x:A]. B[x],
top: Top,
sqequal: s ~ t
Definitions unfolded in proof :
member: t ∈ T,
uall: ∀[x:A]. B[x],
csm-id: 1(X),
csm-id-adjoin: [u],
partial-term-1: u[1]
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-1(H, xx;u) \msim{} partial-term-1(H;u))
Date html generated:
2016_05_19-AM-08_40_10
Last ObjectModification:
2016_04_13-AM-11_12_02
Theory : cubical!type!theory
Home
Index