Nuprl Lemma : prior-latest-val
∀[Info,T:Type]. ∀[X:EClass(T)].  (((X)-)' = (X)' ∈ EClass(T))
Proof
Definitions occuring in Statement : 
es-latest-val: (X)-
, 
es-prior-val: (X)'
, 
eclass: EClass(A[eo; e])
, 
uall: ∀[x:A]. B[x]
, 
universe: Type
, 
equal: s = t ∈ T
Lemmas : 
es-interface-extensionality, 
es-prior-val_wf, 
es-latest-val_wf, 
in-eclass_wf, 
es-prior-interface_wf1, 
es-interface-subtype_rel2, 
es-E_wf, 
event-ordering+_subtype, 
subtype_top, 
es-E-interface_wf, 
top_wf, 
bool_wf, 
eqtt_to_assert, 
bag_size_single_lemma, 
false_wf, 
eqff_to_assert, 
equal_wf, 
bool_cases_sqequal, 
subtype_base_sq, 
bool_subtype_base, 
assert-bnot, 
bag_size_empty_lemma, 
es-le_weakening_eq, 
es-le_wf, 
assert_wf, 
event-ordering+_wf, 
es-locl_wf, 
exists_wf, 
es-locl_transitivity1, 
is-prior-val, 
is-latest-val, 
all_wf, 
iff_wf, 
prior-val-val, 
latest-val-cases, 
es-locl-total, 
eclass-val_wf, 
has-latest-val, 
decidable__es-le, 
decidable__es-locl, 
es-le-not-locl, 
not_assert_elim, 
and_wf, 
assert_elim, 
btrue_neq_bfalse, 
es-locl_transitivity2, 
es-le_weakening
Latex:
\mforall{}[Info,T:Type].  \mforall{}[X:EClass(T)].    (((X)\msupminus{})'  =  (X)')
Date html generated:
2015_07_21-PM-04_21_07
Last ObjectModification:
2015_01_27-PM-05_24_35
Home
Index