Nuprl Lemma : le_int-wf-bar


[x,y:partial(Base)].  (x ≤y ∈ bar(𝔹))


Proof




Definitions occuring in Statement :  bar: bar(T) partial: partial(T) le_int: i ≤j bool: 𝔹 uall: [x:A]. B[x] member: t ∈ T base: Base
Definitions unfolded in proof :  bar: bar(T)
Lemmas referenced :  le_int-wf-partial
Rules used in proof :  cut lemma_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity hypothesis

Latex:
\mforall{}[x,y:partial(Base)].    (x  \mleq{}z  y  \mmember{}  bar(\mBbbB{}))



Date html generated: 2016_07_08-PM-05_18_49
Last ObjectModification: 2016_01_05-PM-11_53_41

Theory : bar!type


Home Index