Nuprl Lemma : bind-return-left
∀[Info,T,S:Type]. ∀[x:T]. ∀f:T ─→ EClass(S). (return-class(x) >z> f[z] = f[x] ∈ EClass(S))
Proof
Definitions occuring in Statement :
return-class: return-class(x),
bind-class: X >x> Y[x],
eclass: EClass(A[eo; e]),
uall: ∀[x:A]. B[x],
so_apply: x[s],
all: ∀x:A. B[x],
function: x:A ─→ B[x],
universe: Type,
equal: s = t ∈ T
Lemmas :
bind-class_wf,
es-E_wf,
event-ordering+_subtype,
event-ordering+_wf,
eclass_wf,
hd-es-le-before-is-first,
btrue_wf,
list_set_type,
tl_wf,
es-le-before_wf2,
subtype_rel_list,
es-le_wf,
not_wf,
assert_wf,
es-first_wf2,
l_all_iff,
Id_wf,
es-loc_wf,
es-le-before_wf,
l_member_wf,
set_wf,
l_member-settype,
equal_wf,
tl-es-le-before,
subtype_rel_self,
list-subtype-bag,
es-le-before-not-null,
list_wf,
list-cases,
null_nil_lemma,
length_of_nil_lemma,
bfalse_wf,
btrue_neq_bfalse,
product_subtype_list,
null_cons_lemma,
length_of_cons_lemma,
length_wf,
non_neg_length,
length_wf_nat,
hd_wf,
subtype_base_sq,
bool_wf,
bool_subtype_base,
bag_wf,
bag-append_wf,
cons_wf,
ge_wf,
iff_weakening_equal,
nil_wf,
subtype_rel_bag,
subtype_rel_sets,
exists_wf,
squash_wf,
true_wf,
sq_stable_from_decidable,
decidable__es-le,
list_ind_cons_lemma,
list_ind_nil_lemma,
reduce_tl_nil_lemma,
reduce_hd_cons_lemma,
reduce_tl_cons_lemma,
subtype_rel_list_set,
es-le-loc,
nat_wf,
return-class_wf,
bag-combine_wf,
eo-forward_wf,
member-eo-forward-E,
bag-combine-append-left,
bag-append-empty,
top_wf,
bag-subtype-list,
single-bag_wf,
empty-bag_wf,
bag-combine-single-left,
bool_cases,
eqtt_to_assert,
eqff_to_assert,
assert_of_bnot,
eo-forward-trivial,
bag-combine-empty-right,
bag_combine_empty_lemma,
equal-wf-T-base
\mforall{}[Info,T,S:Type]. \mforall{}[x:T]. \mforall{}f:T {}\mrightarrow{} EClass(S). (return-class(x) >z> f[z] = f[x])
Date html generated:
2015_07_17-PM-00_43_59
Last ObjectModification:
2015_02_04-PM-05_33_42
Home
Index