Nuprl Lemma : presheaf-snd-at
∀[a,I,p:Top].  (p.2(a) ~ snd(p(a)))
Proof
Definitions occuring in Statement : 
presheaf-snd: p.2
, 
presheaf-term-at: u(a)
, 
uall: ∀[x:A]. B[x]
, 
top: Top
, 
pi2: snd(t)
, 
sqequal: s ~ t
Definitions unfolded in proof : 
presheaf-term-at: u(a)
, 
presheaf-snd: p.2
, 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
Lemmas referenced : 
top_wf
Rules used in proof : 
sqequalSubstitution, 
sqequalRule, 
sqequalReflexivity, 
sqequalTransitivity, 
computationStep, 
isect_memberFormation, 
introduction, 
cut, 
sqequalAxiom, 
extract_by_obid, 
hypothesis, 
sqequalHypSubstitution, 
isect_memberEquality, 
isectElimination, 
thin, 
hypothesisEquality, 
because_Cache
Latex:
\mforall{}[a,I,p:Top].    (p.2(a)  \msim{}  snd(p(a)))
Date html generated:
2018_05_23-AM-08_20_21
Last ObjectModification:
2018_05_20-PM-10_01_00
Theory : presheaf!models!of!type!theory
Home
Index