Nuprl Lemma : equal-top

[x,y:Top].  (x y ∈ Top)


Proof




Definitions occuring in Statement :  uall: [x:A]. B[x] top: Top equal: t ∈ T
Definitions unfolded in proof :  top: Top uall: [x:A]. B[x] member: t ∈ T
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut isect_memberEquality voidElimination voidEquality hypothesis isectEquality sqequalRule sqequalHypSubstitution isectElimination thin hypothesisEquality axiomEquality because_Cache

Latex:
\mforall{}[x,y:Top].    (x  =  y)



Date html generated: 2016_05_13-PM-03_16_09
Last ObjectModification: 2016_01_06-PM-05_20_56

Theory : core_2


Home Index