Nuprl Lemma : primed-class-opt_eq_class-opt-class-primed

[Info,T:Type].

[init:Id

bag(T)].

[X:EClass(T)]. (Prior(X)?init = Prior(X)?

l.init l| |)

Proof not projected

Definitions occuring in Statement : class-opt-class: X?Y, primed-class-opt: Prior(X)?b, primed-class: Prior(X), simple-loc-comb0:

l.b[l]| |, eclass: EClass(A[eo; e]), Id: Id, uall:

[x:A]. B[x], apply: f a, function: x:A

B[x], universe: Type, equal: s = t, bag: bag(T)
Definitions : eclass: EClass(A[eo; e]), primed-class-opt: Prior(X)?b, class-opt-class: X?Y, primed-class: Prior(X), simple-loc-comb0:

l.b[l]| |, simple-loc-comb: F|Loc; Xs|, member: t

T, all:

x:A. B[x], or: P

Q, sq_exists:

x:{A| B[x]}, and: P

Q, implies: P

Q, cand: A c

B, prop:

, iff: P

Q, rev_implies: P

Q, true: True, squash:

T, so_lambda:

x y.t[x; y], ifthenelse: if b then t else f fi , btrue: tt, bfalse: ff, lt_int: i <z j, uall:

[x:A]. B[x], assert:

b, not:

A, nat:

, false: False, so_apply: x[s1;s2], bool:

, unit: Unit, uimplies: b supposing a, uiff: uiff(P;Q), subtype: S

T, it:

Lemmas : es-E_wf, event-ordering+_inc, lt_int_wf, bag-size_wf, nat_wf, es-local-pred_wf, es-locl_wf, assert_wf, not_wf, bag_wf, es-loc_wf, squash_wf, true_wf, empty-bag_wf, eclass_wf, event-ordering+_wf, Id_wf, bag-null_wf, bool_wf, bnot_wf, uiff_transitivity, eqtt_to_assert, assert-bag-null, eqff_to_assert, assert_of_bnot, not_functionality_wrt_uiff

\mforall{}[Info,T:Type]. \mforall{}[init:Id {}\mrightarrow{} bag(T)]. \mforall{}[X:EClass(T)]. (Prior(X)?init = Prior(X)?\mlambda{}l.init l| |) Date html generated: 2011_10_20-PM-03_23_38 Last ObjectModification: 2011_08_16-PM-05_06_14 Home Index