Nuprl Lemma : isallevents_lemma
∀e,eo:Top. (e ∈b E ~ tt)
Proof
Definitions occuring in Statement :
es-all-events: E,
in-eclass: e ∈b X,
btrue: tt,
top: Top,
all: ∀x:A. B[x],
sqequal: s ~ t
Lemmas :
bag_size_single_lemma,
top_wf
\mforall{}e,eo:Top. (e \mmember{}\msubb{} E \msim{} tt)
Date html generated:
2015_07_17-PM-00_54_16
Last ObjectModification:
2015_01_27-PM-10_48_16
Home
Index