Nuprl Lemma : eclass-val_wf

`∀[T:Type]. ∀[A:es:EO+(T) ─→ E ─→ Type]. ∀[X:EClass(A[es;e])]. ∀[eo:EO+(T)]. ∀[e:E].  X(e) ∈ A[eo;e] supposing ↑e ∈b X`

Proof

Definitions occuring in Statement :  eclass-val: `X(e)` in-eclass: `e ∈b X` eclass: `EClass(A[eo; e])` event-ordering+: `EO+(Info)` es-E: `E` assert: `↑b` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` so_apply: `x[s1;s2]` member: `t ∈ T` function: `x:A ─→ B[x]` universe: `Type`
Lemmas :  assert_wf in-eclass_wf dep-eclass_subtype_rel es-E_wf event-ordering+_subtype event-ordering+_wf top_wf subtype_top eclass_wf bag-only_wf2 decidable__lt bag-size_wf nat_wf false_wf le_antisymmetry_iff add_functionality_wrt_le add-zero le-add-cancel equal-wf-T-base assert_of_eq_int eq_int_wf member_wf single-valued-bag-if-le1 le_weakening
\mforall{}[T:Type].  \mforall{}[A:es:EO+(T)  {}\mrightarrow{}  E  {}\mrightarrow{}  Type].  \mforall{}[X:EClass(A[es;e])].  \mforall{}[eo:EO+(T)].  \mforall{}[e:E].
X(e)  \mmember{}  A[eo;e]  supposing  \muparrow{}e  \mmember{}\msubb{}  X

Date html generated: 2015_07_17-PM-00_40_29
Last ObjectModification: 2015_01_27-PM-11_15_50

Home Index