Nuprl Lemma : ycomb-unroll

[f:Top]. (Y (Y f))


Proof




Definitions occuring in Statement :  uall: [x:A]. B[x] top: Top ycomb: Y apply: a sqequal: t
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T ycomb: Y
Lemmas referenced :  top_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalAxiom hypothesis lemma_by_obid sqequalRule

Latex:
\mforall{}[f:Top].  (Y  f  \msim{}  f  (Y  f))



Date html generated: 2016_05_13-PM-03_19_52
Last ObjectModification: 2015_12_26-AM-09_09_16

Theory : sqequal_1


Home Index