Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-07-23 15:16 deb16814

View on Github →

refactor(*): import content from lean/library/data and library_dev

Estimated changes

added theorem eq_iff_sub_eq_zero
added theorem eq_inv_iff_eq_inv
added theorem eq_of_mul_inv_eq_one
added theorem eq_one_of_inv_eq_one
added theorem eq_sub_iff_add_eq
added theorem inv_eq_inv_iff_eq
added theorem inv_eq_one_iff_eq_one
added theorem left_inverse_inv
added theorem mul_eq_iff_eq_inv_mul
added theorem mul_eq_iff_eq_mul_inv
added theorem sub_eq_iff_eq_add
added def gpow
added theorem gpow_add
added theorem gpow_comm
added theorem inv_pow
added def monoid.pow
added theorem mul_pow
added theorem one_pow
added theorem pow_add
added theorem pow_comm
added theorem pow_ge_one_of_ge_one
added def pow_int
added theorem pow_inv_comm
added theorem pow_mul
added def pow_nat
added theorem pow_one
added theorem pow_pos
added theorem pow_sub
added theorem pow_succ'
added theorem pow_succ
added theorem pow_zero
added theorem lattice.bot_inf_eq
added theorem lattice.bot_le
added theorem lattice.bot_sup_eq
added theorem lattice.bot_unique
added theorem lattice.eq_bot_iff
added theorem lattice.eq_top_iff
added theorem lattice.inf_assoc
added theorem lattice.inf_bot_eq
added theorem lattice.inf_comm
added theorem lattice.inf_eq_top_iff
added theorem lattice.inf_idem
added theorem lattice.inf_le_inf
added theorem lattice.inf_le_left
added theorem lattice.inf_le_right
added theorem lattice.inf_of_le_left
added theorem lattice.inf_sup_self
added theorem lattice.inf_top_eq
added theorem lattice.le_inf
added theorem lattice.le_inf_iff
added theorem lattice.le_inf_sup
added theorem lattice.le_of_inf_eq
added theorem lattice.le_of_sup_eq
added theorem lattice.le_sup_left
added theorem lattice.le_sup_right
added theorem lattice.le_top
added theorem lattice.sup_assoc
added theorem lattice.sup_bot_eq
added theorem lattice.sup_comm
added theorem lattice.sup_eq_bot_iff
added theorem lattice.sup_idem
added theorem lattice.sup_inf_le
added theorem lattice.sup_inf_self
added theorem lattice.sup_le
added theorem lattice.sup_le_iff
added theorem lattice.sup_le_sup
added theorem lattice.sup_of_le_left
added theorem lattice.sup_top_eq
added theorem lattice.top_inf_eq
added theorem lattice.top_sup_eq
added theorem lattice.top_unique
added theorem lattice.bot_inf_eq
added theorem lattice.bot_le
added theorem lattice.bot_sup_eq
added theorem lattice.bot_unique
added theorem lattice.eq_bot_iff
added theorem lattice.eq_top_iff
added def lattice.imp
added theorem lattice.inf_assoc
added theorem lattice.inf_bot_eq
added theorem lattice.inf_comm
added theorem lattice.inf_eq_top_iff
added theorem lattice.inf_idem
added theorem lattice.inf_le_inf
added theorem lattice.inf_le_left'
added theorem lattice.inf_le_left
added theorem lattice.inf_le_right'
added theorem lattice.inf_le_right
added theorem lattice.inf_of_le_left
added theorem lattice.inf_sup_self
added theorem lattice.inf_top_eq
added theorem lattice.le_bot_iff
added theorem lattice.le_inf
added theorem lattice.le_inf_iff
added theorem lattice.le_inf_sup
added theorem lattice.le_of_inf_eq
added theorem lattice.le_of_sup_eq
added theorem lattice.le_sup_left'
added theorem lattice.le_sup_left
added theorem lattice.le_sup_right'
added theorem lattice.le_sup_right
added theorem lattice.le_top
added theorem lattice.sup_assoc
added theorem lattice.sup_bot_eq
added theorem lattice.sup_comm
added theorem lattice.sup_eq_bot_iff
added theorem lattice.sup_idem
added theorem lattice.sup_inf_le
added theorem lattice.sup_inf_self
added theorem lattice.sup_le
added theorem lattice.sup_le_iff
added theorem lattice.sup_le_sup
added theorem lattice.sup_of_le_left
added theorem lattice.sup_top_eq
added theorem lattice.top_inf_eq
added theorem lattice.top_le_iff
added theorem lattice.top_sup_eq
added theorem lattice.top_unique
added theorem le_antisymm'
added theorem lattice.inf_neg_eq_bot
added theorem lattice.inf_sup_left
added theorem lattice.inf_sup_right
added theorem lattice.le_sup_inf
added theorem lattice.neg_bot
added theorem lattice.neg_eq_neg_iff
added theorem lattice.neg_inf
added theorem lattice.neg_inf_eq_bot
added theorem lattice.neg_le_neg
added theorem lattice.neg_neg
added theorem lattice.neg_sup
added theorem lattice.neg_sup_eq_top
added theorem lattice.neg_top
added theorem lattice.neg_unique
added theorem lattice.sub_eq
added theorem lattice.sub_eq_left
added theorem lattice.sup_inf_left
added theorem lattice.sup_inf_right
added theorem lattice.sup_neg_eq_top
added theorem lattice.sup_sub_same
added theorem lattice.monotone_and
added theorem lattice.monotone_or
added theorem lattice.monotone_and
added theorem lattice.monotone_or
added theorem lattice.inf_Sup_eq
added theorem lattice.neg_Inf
added theorem lattice.neg_Sup
added theorem lattice.neg_infi
added theorem lattice.neg_supr
added theorem lattice.sup_Inf_eq
added def lattice.Inf
added theorem lattice.Inf_empty
added theorem lattice.Inf_eq_infi
added theorem lattice.Inf_image
added theorem lattice.Inf_insert
added theorem lattice.Inf_le
added theorem lattice.Inf_le_Inf
added theorem lattice.Inf_le_Sup
added theorem lattice.Inf_le_iff
added theorem lattice.Inf_le_of_le
added theorem lattice.Inf_singleton
added theorem lattice.Inf_union
added theorem lattice.Inf_univ
added def lattice.Sup
added theorem lattice.Sup_empty
added theorem lattice.Sup_eq_supr
added theorem lattice.Sup_image
added theorem lattice.Sup_insert
added theorem lattice.Sup_inter_le
added theorem lattice.Sup_le
added theorem lattice.Sup_le_Sup
added theorem lattice.Sup_singleton
added theorem lattice.Sup_union
added theorem lattice.Sup_univ
added def lattice.infi
added theorem lattice.infi_and
added theorem lattice.infi_comm
added theorem lattice.infi_const
added theorem lattice.infi_empty
added theorem lattice.infi_emptyset
added theorem lattice.infi_exists
added theorem lattice.infi_false
added theorem lattice.infi_inf_eq
added theorem lattice.infi_insert
added theorem lattice.infi_le
added theorem lattice.infi_le_infi2
added theorem lattice.infi_le_infi
added theorem lattice.infi_le_of_le
added theorem lattice.infi_or
added theorem lattice.infi_prod
added theorem lattice.infi_sigma
added theorem lattice.infi_singleton
added theorem lattice.infi_subtype
added theorem lattice.infi_sum
added theorem lattice.infi_true
added theorem lattice.infi_union
added theorem lattice.infi_unit
added theorem lattice.infi_univ
added theorem lattice.le_Inf
added theorem lattice.le_Inf_inter
added theorem lattice.le_Sup
added theorem lattice.le_Sup_iff
added theorem lattice.le_Sup_of_le
added theorem lattice.le_infi
added theorem lattice.le_infi_iff
added theorem lattice.le_supr
added theorem lattice.le_supr_of_le
added def lattice.supr
added theorem lattice.supr_and
added theorem lattice.supr_comm
added theorem lattice.supr_const
added theorem lattice.supr_empty
added theorem lattice.supr_emptyset
added theorem lattice.supr_exists
added theorem lattice.supr_false
added theorem lattice.supr_insert
added theorem lattice.supr_le
added theorem lattice.supr_le_iff
added theorem lattice.supr_le_supr2
added theorem lattice.supr_le_supr
added theorem lattice.supr_or
added theorem lattice.supr_prod
added theorem lattice.supr_sigma
added theorem lattice.supr_singleton
added theorem lattice.supr_subtype
added theorem lattice.supr_sum
added theorem lattice.supr_sup_eq
added theorem lattice.supr_true
added theorem lattice.supr_union
added theorem lattice.supr_unit
added theorem lattice.supr_univ
added theorem set.subset_union_left
added theorem set.subset_union_right
added theorem insert_def
added theorem insert_eq_of_mem
added theorem insert_of_has_insert
added theorem inter_def
added theorem inter_left_comm
added def lattice.Inf
added theorem lattice.Inf_empty
added theorem lattice.Inf_eq_infi
added theorem lattice.Inf_image
added theorem lattice.Inf_insert
added theorem lattice.Inf_le
added theorem lattice.Inf_le_Inf
added theorem lattice.Inf_le_Sup
added theorem lattice.Inf_le_iff
added theorem lattice.Inf_le_of_le
added theorem lattice.Inf_singleton
added theorem lattice.Inf_union
added theorem lattice.Inf_univ
added def lattice.Sup
added theorem lattice.Sup_empty
added theorem lattice.Sup_eq_supr
added theorem lattice.Sup_image
added theorem lattice.Sup_insert
added theorem lattice.Sup_inter_le
added theorem lattice.Sup_le
added theorem lattice.Sup_le_Sup
added theorem lattice.Sup_singleton
added theorem lattice.Sup_union
added theorem lattice.Sup_univ
added theorem lattice.foo'
added theorem lattice.foo
added def lattice.infi
added theorem lattice.infi_and
added theorem lattice.infi_comm
added theorem lattice.infi_const
added theorem lattice.infi_empty
added theorem lattice.infi_emptyset
added theorem lattice.infi_exists
added theorem lattice.infi_false
added theorem lattice.infi_inf_eq
added theorem lattice.infi_insert
added theorem lattice.infi_le'
added theorem lattice.infi_le
added theorem lattice.infi_le_infi2
added theorem lattice.infi_le_infi
added theorem lattice.infi_le_of_le
added theorem lattice.infi_or
added theorem lattice.infi_prod
added theorem lattice.infi_sigma
added theorem lattice.infi_singleton
added theorem lattice.infi_subtype
added theorem lattice.infi_sum
added theorem lattice.infi_true
added theorem lattice.infi_union
added theorem lattice.infi_unit
added theorem lattice.infi_univ
added theorem lattice.le_Inf
added theorem lattice.le_Inf_inter
added theorem lattice.le_Sup
added theorem lattice.le_Sup_iff
added theorem lattice.le_Sup_of_le
added theorem lattice.le_infi
added theorem lattice.le_infi_iff
added theorem lattice.le_supr'
added theorem lattice.le_supr
added theorem lattice.le_supr_of_le
added def lattice.supr
added theorem lattice.supr_and
added theorem lattice.supr_comm
added theorem lattice.supr_const
added theorem lattice.supr_empty
added theorem lattice.supr_emptyset
added theorem lattice.supr_exists
added theorem lattice.supr_false
added theorem lattice.supr_insert
added theorem lattice.supr_le
added theorem lattice.supr_le_iff
added theorem lattice.supr_le_supr2
added theorem lattice.supr_le_supr
added theorem lattice.supr_or
added theorem lattice.supr_prod
added theorem lattice.supr_sigma
added theorem lattice.supr_singleton
added theorem lattice.supr_subtype
added theorem lattice.supr_sum
added theorem lattice.supr_sup_eq
added theorem lattice.supr_true
added theorem lattice.supr_union
added theorem lattice.supr_unit
added theorem lattice.supr_univ
added theorem mem_insert_iff
added theorem mem_inter_eq
added theorem mem_set_of
added theorem mem_set_of_eq
added theorem mem_singleton
added theorem mem_singleton_iff
added theorem mem_union_eq
added theorem mem_univ_eq
added theorem nmem_set_of_eq
added theorem set_eq_def
added theorem set_of_false
added theorem singleton_def
added theorem subset_def
added theorem subset_insert
added theorem subset_univ
added theorem union_def
added theorem union_left_comm
added theorem Union_subset_Union2
added theorem Union_subset_Union
added theorem bind_assoc
added theorem compl_image_set_of
added theorem diff_empty
added theorem diff_neq_empty
added def directed
added theorem directed_of_chain
added def directed_on
added theorem directed_on_Union
added theorem eq_of_sup_eq_inf_eq
added theorem filter.Inter_mem_sets
added def filter.at_bot
added def filter.at_top
added theorem filter.bind_def
added theorem filter.bind_mono2
added theorem filter.bind_mono
added theorem filter.bind_sup
added theorem filter.binfi_sup_eq
added def filter.cofinite
added theorem filter.filter_eq
added theorem filter.fmap_principal
added theorem filter.image_mem_map
added theorem filter.inf_principal
added theorem filter.infi_sets_eq'
added theorem filter.infi_sets_eq
added theorem filter.infi_sup_eq
added theorem filter.inter_mem_sets
added def filter.join
added theorem filter.le_lift'
added theorem filter.le_map_vmap
added theorem filter.le_vmap_map
added theorem filter.lift'_cong
added theorem filter.lift'_id
added theorem filter.lift'_infi
added theorem filter.lift'_mono'
added theorem filter.lift'_mono
added theorem filter.lift'_principal
added theorem filter.lift_assoc
added theorem filter.lift_comm
added theorem filter.lift_infi'
added theorem filter.lift_infi
added theorem filter.lift_mono'
added theorem filter.lift_mono
added theorem filter.lift_principal
added theorem filter.lift_sets_eq
added def filter.map
added theorem filter.map_binfi_eq
added theorem filter.map_bot
added theorem filter.map_compose
added theorem filter.map_eq_bot_iff
added theorem filter.map_id
added theorem filter.map_infi_eq
added theorem filter.map_infi_le
added theorem filter.map_lift'_eq2
added theorem filter.map_lift'_eq
added theorem filter.map_lift_eq2
added theorem filter.map_lift_eq
added theorem filter.map_mono
added theorem filter.map_principal
added theorem filter.map_sup
added theorem filter.map_vmap_le
added theorem filter.mem_bind_sets
added theorem filter.mem_bot_sets
added theorem filter.mem_inf_sets
added theorem filter.mem_infi_sets
added theorem filter.mem_join_sets
added theorem filter.mem_lift'
added theorem filter.mem_lift'_iff
added theorem filter.mem_lift
added theorem filter.mem_lift_iff
added theorem filter.mem_map
added theorem filter.mem_prod_iff
added theorem filter.mem_pure
added theorem filter.mem_return_sets
added theorem filter.mem_sup_sets
added theorem filter.mem_vmap_of_mem
added theorem filter.monotone_lift'
added theorem filter.monotone_lift
added theorem filter.monotone_map
added theorem filter.monotone_vmap
added def filter.principal
added theorem filter.principal_bind
added theorem filter.principal_empty
added theorem filter.principal_mono
added theorem filter.principal_univ
added theorem filter.prod_comm
added theorem filter.prod_inf_prod
added theorem filter.prod_lift_lift
added theorem filter.prod_map_map_eq
added theorem filter.prod_mem_prod
added theorem filter.prod_mono
added theorem filter.prod_neq_bot
added theorem filter.prod_same_eq
added theorem filter.pure_def
added theorem filter.return_neq_bot
added theorem filter.seq_mono
added theorem filter.sup_join
added theorem filter.sup_principal
added theorem filter.supr_join
added theorem filter.supr_map
added theorem filter.supr_principal
added theorem filter.supr_sets_eq
added def filter.towards
added theorem filter.ultrafilter_map
added theorem filter.univ_mem_sets'
added theorem filter.univ_mem_sets
added theorem filter.vimage_mem_vmap
added def filter.vmap
added theorem filter.vmap_eq_lift'
added theorem filter.vmap_lift'_eq2
added theorem filter.vmap_lift'_eq
added theorem filter.vmap_lift_eq2
added theorem filter.vmap_lift_eq
added theorem filter.vmap_map
added theorem filter.vmap_mono
added theorem filter.vmap_neq_bot
added theorem filter.vmap_principal
added theorem filter.vmap_vmap_comp
added structure filter
added theorem lattice.Sup_le_iff
added theorem map_bind
added theorem not_not_mem_iff
added theorem prod.fst_swap
added theorem prod.mk.eta
added theorem prod.snd_swap
added def prod.swap
added theorem prod.swap_prod_mk
added theorem prod.swap_swap
added theorem prod.swap_swap_eq
added theorem pure_seq_eq_map
added theorem sUnion_eq_Union
added theorem sUnion_mono
added theorem seq_bind_eq
added theorem seq_eq_bind_map
added theorem set.bind_def
added theorem set.fmap_eq_image
added theorem set.image_swap_prod
added theorem set.mem_prod_eq
added theorem set.mem_seq_iff
added theorem set.monotone_inter
added theorem set.monotone_prod
added theorem set.monotone_set_of
added theorem set.prod_inter_prod
added theorem set.prod_mono
added theorem set.prod_neq_empty_iff
added theorem set.prod_vimage_eq
added theorem set.set_of_mem_eq
added theorem set.vimage_set_of_eq
added theorem singleton_neq_emptyset
added def upwards
added theorem ge_of_eq
added def lattice.gfp
added theorem lattice.gfp_comp
added theorem lattice.gfp_eq
added theorem lattice.gfp_gfp
added theorem lattice.gfp_induct
added theorem lattice.gfp_le
added theorem lattice.le_gfp
added theorem lattice.le_lfp
added def lattice.lfp
added theorem lattice.lfp_comp
added theorem lattice.lfp_eq
added theorem lattice.lfp_induct
added theorem lattice.lfp_le
added theorem lattice.lfp_lfp
added theorem lattice.monotone_gfp
added theorem lattice.monotone_lfp
added def zorn.chain
added inductive zorn.chain_closure
added theorem zorn.chain_insert
added theorem zorn.chain_succ
added def zorn.max_chain
added theorem zorn.max_chain_spec
added def zorn.succ_chain
added theorem zorn.succ_increasing
added theorem zorn.succ_spec
added def zorn.super_chain
added theorem zorn.super_of_not_max
added theorem zorn.zorn
added theorem zorn.zorn_weak_order
added theorem le_dual_eq_le
added theorem le_max_left_iff_true
added theorem le_max_right_iff_true
added theorem max.left_comm
added theorem max.right_comm
added theorem min_right_comm
added def monotone
added theorem monotone_app
added theorem monotone_comp
added theorem monotone_const
added theorem monotone_id
added theorem monotone_lam
added def weak_order_dual
added theorem mul_neg_one_eq_neg
added def bitvec.adc
added def bitvec.add_lsb
added def bitvec.and
added def bitvec.append
added def bitvec.fill_shr
added def bitvec.not
added theorem bitvec.of_nat_succ
added def bitvec.or
added def bitvec.sbb
added def bitvec.sborrow
added def bitvec.sge
added def bitvec.sgt
added def bitvec.shl
added def bitvec.sle
added def bitvec.slt
added def bitvec.sshr
added theorem bitvec.to_nat_append
added theorem bitvec.to_nat_of_nat
added def bitvec.uborrow
added def bitvec.uge
added def bitvec.ugt
added def bitvec.ule
added def bitvec.ult
added def bitvec.ushr
added def bitvec.xor
added def bitvec
added theorem bool.band_assoc
added theorem bool.band_comm
added theorem bool.band_elim_left
added theorem bool.band_elim_right
added theorem bool.band_eq_ff
added theorem bool.band_eq_tt
added theorem bool.band_ff
added theorem bool.band_intro
added theorem bool.band_left_comm
added theorem bool.band_self
added theorem bool.band_tt
added theorem bool.bnot_bnot
added theorem bool.bnot_false
added theorem bool.bnot_true
added theorem bool.bor_assoc
added theorem bool.bor_comm
added theorem bool.bor_eq_ff
added theorem bool.bor_eq_tt
added theorem bool.bor_ff
added theorem bool.bor_inl
added theorem bool.bor_inr
added theorem bool.bor_left_comm
added theorem bool.bor_tt
added def bool.bxor
added theorem bool.bxor_assoc
added theorem bool.bxor_comm
added theorem bool.bxor_ff
added theorem bool.bxor_left_comm
added theorem bool.bxor_self
added theorem bool.bxor_tt
added theorem bool.coe_tt
added theorem bool.cond_ff
added theorem bool.cond_tt
added theorem bool.dichotomy
added theorem bool.eq_ff_of_ne_tt
added theorem bool.eq_tt_of_ne_ff
added theorem bool.ff_band
added theorem bool.ff_bor
added theorem bool.ff_bxor
added theorem bool.ff_bxor_ff
added theorem bool.ff_bxor_tt
added theorem bool.or_of_bor_eq
added theorem bool.tt_band
added theorem bool.tt_bor
added theorem bool.tt_bxor
added theorem bool.tt_bxor_ff
added theorem bool.tt_bxor_tt
added theorem lt_succ_of_lt
added def raise_fin
added theorem bucket_array.foldl_eq
added def bucket_array
added theorem hash_map.contains_iff
added def hash_map.entries
added theorem hash_map.entries_empty
added def hash_map.erase
added def hash_map.find
added theorem hash_map.find_aux_iff
added theorem hash_map.find_empty
added theorem hash_map.find_erase
added theorem hash_map.find_erase_eq
added theorem hash_map.find_erase_ne
added theorem hash_map.find_iff
added theorem hash_map.find_insert
added def hash_map.fold
added def hash_map.insert
added theorem hash_map.insert_lemma
added def hash_map.keys
added theorem hash_map.keys_empty
added theorem hash_map.mem_erase
added theorem hash_map.mem_insert
added theorem hash_map.mk_as_list
added def hash_map.mk_idx
added def hash_map.of_list
added theorem hash_map.valid.eq'
added theorem hash_map.valid.eq
added theorem hash_map.valid.erase
added theorem hash_map.valid.insert
added theorem hash_map.valid.mk
added theorem hash_map.valid.modify
added theorem hash_map.valid.nodup
added theorem hash_map.valid.replace
added def hash_map.valid
added theorem hash_map.valid_aux.eq
added inductive hash_map.valid_aux
added structure hash_map
added def mk_hash_map
added theorem int.neg_add_neg
added theorem neg_nat_succ
added theorem neg_pred
added theorem neg_succ
added theorem neg_succ_of_nat_eq'
added theorem of_nat_sub
added def pred
added theorem pred_nat_succ
added theorem pred_neg_pred
added theorem pred_succ
added def rec_nat_on
added theorem rec_nat_on_neg
added def succ
added theorem succ_neg_nat_succ
added theorem succ_neg_succ
added theorem succ_pred
added def lazy_list.append
added def lazy_list.approx
added def lazy_list.filter
added def lazy_list.for
added def lazy_list.head
added def lazy_list.join
added def lazy_list.map
added def lazy_list.map₂
added def lazy_list.nth
added def lazy_list.tail
added def lazy_list.zip
added inductive lazy_list
added theorem list.append.assoc
added theorem list.append_concat
added theorem list.concat_append
added theorem list.concat_cons
added theorem list.concat_ne_nil
added theorem list.concat_nil
added theorem list.cons_inj
added theorem list.cons_ne_nil
added def list.count
added theorem list.count_append
added theorem list.count_concat
added theorem list.count_cons'
added theorem list.count_cons
added theorem list.count_cons_of_ne
added theorem list.count_cons_self
added theorem list.count_nil
added theorem list.count_pos_of_mem
added theorem list.count_singleton
added theorem list.head_cons
added theorem list.index_of_cons
added theorem list.index_of_nil
added theorem list.index_of_nth
added def list.inth
added theorem list.inth_succ
added theorem list.inth_zero
added def list.ith
added theorem list.ith_succ
added theorem list.ith_zero
added theorem list.last_congr
added theorem list.last_cons_cons
added theorem list.last_singleton
added theorem list.length_taken_le
added theorem list.mem_iff_count_pos
added theorem list.mem_of_count_pos
added theorem list.nth_eq_some
added theorem list.tail_cons
added theorem list.tail_nil
added theorem list.taken_all
added theorem list.taken_all_of_ge
added theorem list.taken_cons
added theorem list.taken_nil
added theorem list.taken_zero
added theorem list.all_cons
added theorem list.all_eq_tt_iff
added theorem list.all_nil
added theorem list.any_cons
added theorem list.any_eq_tt_iff
added theorem list.any_nil
added theorem list.any_of_mem
added def list.dinj
added def list.dinj₁
added def list.dmap
added theorem list.dmap_cons_of_neg
added theorem list.dmap_cons_of_pos
added theorem list.dmap_nil
added def list.flat
added theorem list.foldl_append
added theorem list.foldl_cons
added theorem list.foldl_eq_foldr
added theorem list.foldl_nil
added theorem list.foldl_reverse
added theorem list.foldr_append
added theorem list.foldr_cons
added theorem list.foldr_nil
added theorem list.foldr_reverse
added theorem list.forall_mem_cons
added theorem list.forall_mem_nil
added theorem list.length_mapAccumR
added theorem list.length_map_accumr
added theorem list.length_product
added theorem list.length_replicate
added def list.mapAccumR
added def list.map_accumr
added theorem list.map₂_nil1
added theorem list.map₂_nil2
added theorem list.mem_dmap
added theorem list.mem_product
added theorem list.nil_product
added def list.product
added theorem list.product_cons
added theorem list.product_nil
added def list.replicate
added theorem list.unzip_cons'
added theorem list.unzip_cons
added theorem list.unzip_nil
added theorem list.zip_cons_cons
added theorem list.zip_nil_left
added theorem list.zip_nil_right
added theorem list.zip_unzip
added theorem list.perm.eqv
added theorem list.perm.mem_of_perm
added theorem list.perm.perm_app
added theorem list.perm.perm_app_inv
added theorem list.perm.perm_erase
added theorem list.perm.perm_ext
added theorem list.perm.perm_filter
added theorem list.perm.perm_insert
added theorem list.perm.perm_inter
added theorem list.perm.perm_map
added theorem list.perm.perm_middle
added theorem list.perm.perm_of_qeq
added theorem list.perm.perm_product
added theorem list.perm.perm_rev
added theorem list.perm.perm_union
added inductive list.perm.qeq
added theorem list.perm.qeq_app
added theorem list.perm.qeq_of_mem
added theorem list.perm.qeq_split
added theorem list.perm.xswap
added inductive list.perm
added theorem list.disjoint.comm
added def list.disjoint
added theorem list.disjoint_left
added theorem list.disjoint_nil_left
added theorem list.disjoint_right
added theorem list.erase_append_left
added theorem list.erase_cons
added theorem list.erase_cons_head
added theorem list.erase_cons_tail
added def list.erase_dup
added theorem list.erase_dup_nil
added theorem list.erase_dup_sublist
added theorem list.erase_dup_subset
added theorem list.erase_nil
added theorem list.erase_of_not_mem
added theorem list.erase_sublist
added theorem list.erase_subset
added theorem list.forall_mem_union
added theorem list.insert.def
added theorem list.insert_nil
added theorem list.insert_of_mem
added theorem list.insert_of_not_mem
added theorem list.inter_cons_of_mem
added theorem list.inter_nil
added theorem list.length_upto
added theorem list.lt_of_mem_upto
added theorem list.mem_erase_dup
added theorem list.mem_erase_dup_iff
added theorem list.mem_insert_iff
added theorem list.mem_insert_of_mem
added theorem list.mem_insert_self
added theorem list.mem_inter_iff
added theorem list.mem_of_mem_erase
added theorem list.mem_union_iff
added theorem list.mem_union_left
added theorem list.mem_union_right
added theorem list.mem_upto_of_lt
added inductive list.nodup
added theorem list.nodup_app_comm
added theorem list.nodup_concat
added theorem list.nodup_cons
added theorem list.nodup_erase_dup
added theorem list.nodup_filter
added theorem list.nodup_head
added theorem list.nodup_insert
added theorem list.nodup_map
added theorem list.nodup_middle
added theorem list.nodup_nil
added theorem list.nodup_of_sublist
added theorem list.nodup_product
added theorem list.nodup_singleton
added theorem list.nodup_upto
added theorem list.subset_erase_dup
added theorem list.union_cons
added theorem list.union_nil
added def list.upto
added theorem list.upto_nil
added theorem list.upto_step
added theorem list.upto_succ
added theorem list.length_split_le
added theorem list.length_split_lt
added def list.merge
added def list.merge_sort
added theorem list.perm_merge
added theorem list.perm_merge_sort
added theorem list.perm_split
added def list.sorted
added theorem list.sorted_cons
added theorem list.sorted_merge
added theorem list.sorted_merge_sort
added theorem list.sorted_nil
added theorem list.sorted_singleton
added def list.split
added theorem list.split_cons_of_eq
added theorem nat.add_pos_left
added theorem nat.add_pos_right
added theorem nat.lt_succ_iff_le
added theorem nat.succ_le_succ_iff
added def iterate
added theorem nat.add_eq_addl
added theorem nat.add_one
added theorem nat.add_one_ne_zero
added def nat.addl
added theorem nat.addl_succ_left
added theorem nat.addl_succ_right
added theorem nat.addl_zero_left
added theorem nat.addl_zero_right
added theorem nat.discriminate
added theorem nat.one_add
added theorem nat.one_succ_zero
added theorem nat.sub_induction
added theorem nat.succ_inj
added theorem nat.two_step_induction
added theorem nat.zero_has_zero
added def ball'
added def ball
added theorem ball_of_ball_succ'
added theorem ball_of_ball_succ
added theorem ball_succ_of_ball
added theorem ball_zero'
added theorem ball_zero
added theorem not_ball_of_not
added def step_p
added theorem nat.comprime_one_left
added theorem nat.comprime_one_right
added theorem nat.coprime_mul
added theorem nat.coprime_mul_right
added theorem nat.coprime_of_dvd'
added theorem nat.coprime_of_dvd
added theorem nat.coprime_pow
added theorem nat.coprime_pow_left
added theorem nat.coprime_pow_right
added theorem nat.coprime_swap
added theorem nat.dvd_gcd
added theorem nat.dvd_lcm_left
added theorem nat.dvd_lcm_right
added theorem nat.exists_coprime
added theorem nat.gcd_assoc
added theorem nat.gcd_comm
added theorem nat.gcd_div
added theorem nat.gcd_dvd
added theorem nat.gcd_dvd_left
added theorem nat.gcd_dvd_right
added theorem nat.gcd_mul_lcm
added theorem nat.gcd_mul_left
added theorem nat.gcd_mul_right
added theorem nat.gcd_one_right
added theorem nat.lcm_assoc
added theorem nat.lcm_comm
added theorem nat.lcm_dvd
added theorem nat.lcm_one_left
added theorem nat.lcm_one_right
added theorem nat.lcm_self
added theorem nat.lcm_zero_left
added theorem nat.lcm_zero_right
added theorem nat.dist.def
added def nat.dist
added theorem nat.dist_add_add_left
added theorem nat.dist_add_add_right
added theorem nat.dist_comm
added theorem nat.dist_eq_intro
added theorem nat.dist_eq_sub_of_ge
added theorem nat.dist_eq_sub_of_le
added theorem nat.dist_eq_zero
added theorem nat.dist_mul_left
added theorem nat.dist_mul_right
added theorem nat.dist_pos_of_ne
added theorem nat.dist_self
added theorem nat.dist_succ_succ
added theorem nat.dist_zero_left
added theorem nat.dist_zero_right
added theorem nat.eq_of_dist_eq_zero
added def cast_num
added def cast_pos_num
added def int.of_snum
added def int.of_znum
added def nat.of_num
added def nat.of_pos_num
added def num.bit
added def num.cmp
added def num.of_nat
added def num.pred
added def num.size
added def num.succ'
added def num.succ
added def num.to_znum
added inductive num
added def nzsnum.bit0
added def nzsnum.bit1
added def nzsnum.drec'
added def nzsnum.head
added def nzsnum.not
added def nzsnum.sign
added def nzsnum.tail
added inductive nzsnum
added def pos_num.bit
added def pos_num.cmp
added def pos_num.is_one
added def pos_num.of_nat
added def pos_num.pred'
added def pos_num.pred
added def pos_num.psub
added def pos_num.size
added def pos_num.succ
added inductive pos_num
added def snum.bit0
added def snum.bit1
added def snum.bit
added theorem snum.bit_one
added theorem snum.bit_zero
added def snum.bits
added def snum.cadd
added def snum.czadd
added def snum.drec'
added def snum.head
added def snum.not
added def snum.pred
added def snum.rec'
added def snum.sign
added def snum.succ
added def snum.tail
added def snum.test_bit
added inductive snum
added def znum.pred
added def znum.succ
added def znum.zneg
added inductive znum
added def num.land
added def num.ldiff
added def num.lor
added def num.lxor
added def num.one_bits
added def num.shiftl
added def num.shiftr
added def num.test_bit
added def pos_num.land
added def pos_num.ldiff
added def pos_num.lor
added def pos_num.lxor
added def pos_num.one_bits
added def pos_num.shiftl
added def pos_num.shiftr
added def pos_num.test_bit
added theorem num.add_of_nat
added theorem num.add_succ
added theorem num.add_to_nat
added theorem num.add_zero
added theorem num.bit_to_nat
added theorem num.bitwise_to_nat
added theorem num.cmp_dec
added theorem num.cmp_swap
added theorem num.land_to_nat
added theorem num.ldiff_to_nat
added theorem num.le_iff_cmp
added theorem num.lor_to_nat
added theorem num.lt_iff_cmp
added theorem num.lxor_to_nat
added theorem num.mul_to_nat
added theorem num.of_nat_inj
added theorem num.of_to_nat
added theorem num.one_to_nat
added theorem num.pred_to_nat
added theorem num.shiftl_to_nat
added theorem num.shiftr_to_nat
added theorem num.succ'_to_nat
added theorem num.succ_to_nat
added theorem num.test_bit_to_nat
added theorem num.to_nat_inj
added theorem num.to_of_nat
added theorem num.zero_add
added theorem num.zero_to_nat
added theorem pos_num.add_one
added theorem pos_num.add_succ
added theorem pos_num.add_to_nat
added theorem pos_num.bit0_of_bit0
added theorem pos_num.bit1_of_bit1
added theorem pos_num.bit_to_nat
added theorem pos_num.cmp_dec
added theorem pos_num.cmp_dec_lemma
added theorem pos_num.cmp_swap
added theorem pos_num.le_iff_cmp
added theorem pos_num.lt_iff_cmp
added theorem pos_num.mul_to_nat
added theorem pos_num.of_to_nat
added theorem pos_num.one_add
added theorem pos_num.one_to_nat
added theorem pos_num.pred'_to_nat
added theorem pos_num.pred_to_nat
added theorem pos_num.succ_to_nat
added theorem pos_num.to_nat_inj
added theorem pos_num.to_nat_pos
added def pfun.as_subtype
added theorem pfun.bind_defined
added def pfun.dom
added theorem pfun.dom_iff_graph
added def pfun.eval_opt
added def pfun.fn
added def pfun.graph
added theorem pfun.pure_defined
added def pfun.ran
added def pfun.restrict
added def pfun
added def roption.assert
added theorem roption.assert_defined
added theorem roption.bind_assoc
added theorem roption.bind_defined
added theorem roption.dom_iff_mem
added theorem roption.eq_ret_of_mem
added theorem roption.mem_bind
added theorem roption.mem_ret
added theorem roption.mem_ret_iff
added theorem roption.mem_some
added theorem roption.mem_unique
added theorem roption.of_to_option
added def roption.restrict
added theorem roption.some_bind
added theorem roption.to_of_option
added structure roption
added def nat.succ_pnat
added def nat.to_pnat'
added def nat.to_pnat
added theorem pnat.nat_coe_val
added theorem pnat.to_pnat'_coe
added theorem pnat.to_pnat'_val
added def pnat
added theorem not_antimono
added def rat
added def computation.bind
added theorem computation.bind_assoc
added theorem computation.bind_congr
added theorem computation.bind_ret'
added theorem computation.bind_ret
added theorem computation.equiv.refl
added theorem computation.equiv.symm
added def computation.get
added theorem computation.get_bind
added theorem computation.get_equiv
added theorem computation.get_ret
added theorem computation.get_think
added theorem computation.get_thinkN
added def computation.head
added theorem computation.head_empty
added theorem computation.head_ret
added theorem computation.head_think
added def computation.join
added theorem computation.le_stable
added theorem computation.length_ret
added def computation.lmap
added def computation.map
added theorem computation.map_comp
added theorem computation.map_congr
added theorem computation.map_id
added theorem computation.map_ret'
added theorem computation.map_ret
added theorem computation.map_think'
added theorem computation.map_think
added theorem computation.mem_bind
added theorem computation.mem_map
added theorem computation.mem_unique
added theorem computation.orelse_ret
added theorem computation.ret_bind
added theorem computation.ret_mem
added theorem computation.ret_orelse
added theorem computation.return_def
added def computation.rmap
added def computation.tail
added theorem computation.tail_empty
added theorem computation.tail_ret
added theorem computation.tail_think
added theorem computation.thinkN_mem
added theorem computation.think_bind
added theorem computation.think_mem
added def computation
added def seq.append
added theorem seq.append_assoc
added theorem seq.append_nil
added def seq.bisim_o
added def seq.cases_on
added theorem seq.coinduction2
added theorem seq.coinduction
added def seq.cons
added theorem seq.cons_append
added def seq.corec.F
added def seq.corec
added def seq.corec_eq
added def seq.destruct
added theorem seq.destruct_cons
added theorem seq.destruct_eq_cons
added theorem seq.destruct_eq_nil
added theorem seq.destruct_nil
added def seq.drop
added theorem seq.dropn_add
added theorem seq.dropn_tail
added theorem seq.eq_of_bisim
added theorem seq.exists_of_mem_map
added def seq.head
added theorem seq.head_cons
added theorem seq.head_dropn
added theorem seq.head_eq_destruct
added theorem seq.head_nil
added def seq.join
added theorem seq.join_append
added theorem seq.join_cons
added theorem seq.join_cons_cons
added theorem seq.join_cons_nil
added theorem seq.join_nil
added theorem seq.le_stable
added def seq.map
added theorem seq.map_append
added theorem seq.map_comp
added theorem seq.map_cons
added theorem seq.map_id
added theorem seq.map_nil
added theorem seq.map_nth
added theorem seq.map_tail
added theorem seq.mem_cons
added theorem seq.mem_cons_iff
added theorem seq.mem_cons_of_mem
added theorem seq.mem_map
added theorem seq.mem_rec_on
added def seq.nil
added theorem seq.nil_append
added theorem seq.not_mem_nil
added def seq.nth
added theorem seq.nth_tail
added def seq.of_lazy_list
added def seq.of_list
added def seq.of_list_cons
added def seq.of_list_nil
added def seq.of_stream
added def seq.omap
added def seq.split_at
added def seq.tail
added theorem seq.tail_cons
added theorem seq.tail_nil
added def seq.take
added def seq.to_list'
added def seq.to_list
added def seq.to_stream
added def seq.unzip
added def seq.zip
added def seq.zip_with
added def seq1.bind
added theorem seq1.bind_assoc
added theorem seq1.bind_ret
added def seq1.join
added theorem seq1.join_cons
added theorem seq1.join_join
added theorem seq1.join_map_ret
added theorem seq1.join_nil
added def seq1.map
added theorem seq1.map_id
added theorem seq1.map_join'
added theorem seq1.map_join
added def seq1.ret
added theorem seq1.ret_bind
added def seq1.to_seq
added def seq1
added def seq
added def wseq.all
added def wseq.any
added def wseq.append
added theorem wseq.append_assoc
added theorem wseq.append_nil
added def wseq.bind
added theorem wseq.bind_assoc
added theorem wseq.bind_congr
added theorem wseq.bind_ret
added theorem wseq.bisim_o.imp
added def wseq.bisim_o
added def wseq.cases_on
added def wseq.collect
added def wseq.compute
added def wseq.cons
added theorem wseq.cons_append
added theorem wseq.cons_congr
added def wseq.destruct
added theorem wseq.destruct_append
added theorem wseq.destruct_congr
added theorem wseq.destruct_cons
added theorem wseq.destruct_dropn
added theorem wseq.destruct_flatten
added theorem wseq.destruct_join
added theorem wseq.destruct_map
added theorem wseq.destruct_nil
added theorem wseq.destruct_of_seq
added theorem wseq.destruct_tail
added theorem wseq.destruct_think
added def wseq.drop.aux
added def wseq.drop
added theorem wseq.dropn_add
added theorem wseq.dropn_congr
added theorem wseq.dropn_cons
added theorem wseq.dropn_nil
added theorem wseq.dropn_of_seq
added theorem wseq.dropn_tail
added theorem wseq.dropn_think
added theorem wseq.eq_or_mem_iff_mem
added theorem wseq.equiv.equivalence
added theorem wseq.equiv.ext
added theorem wseq.equiv.refl
added theorem wseq.equiv.symm
added theorem wseq.equiv.trans
added def wseq.equiv
added theorem wseq.exists_nth_of_mem
added theorem wseq.exists_of_mem_map
added def wseq.filter
added def wseq.filter_map
added def wseq.find
added def wseq.find_index
added def wseq.flatten
added theorem wseq.flatten_congr
added theorem wseq.flatten_equiv
added theorem wseq.flatten_ret
added theorem wseq.flatten_think
added def wseq.get
added def wseq.head
added theorem wseq.head_congr
added theorem wseq.head_cons
added theorem wseq.head_nil
added theorem wseq.head_of_seq
added theorem wseq.head_think
added def wseq.index_of
added def wseq.indexes_of
added def wseq.inits
added def wseq.is_empty
added def wseq.is_finite
added def wseq.join
added theorem wseq.join_append
added theorem wseq.join_congr
added def wseq.join_cons
added theorem wseq.join_join
added theorem wseq.join_map_ret
added def wseq.join_nil
added theorem wseq.join_ret
added def wseq.join_think
added def wseq.length
added theorem wseq.length_eq_map
added def wseq.lift_rel
added theorem wseq.lift_rel_append
added theorem wseq.lift_rel_bind
added theorem wseq.lift_rel_destruct
added theorem wseq.lift_rel_flatten
added theorem wseq.lift_rel_join.lem
added theorem wseq.lift_rel_join
added theorem wseq.lift_rel_map
added theorem wseq.lift_rel_o.imp
added def wseq.lift_rel_o
added def wseq.map
added theorem wseq.map_append
added theorem wseq.map_comp
added theorem wseq.map_congr
added theorem wseq.map_cons
added theorem wseq.map_id
added theorem wseq.map_join
added theorem wseq.map_nil
added theorem wseq.map_ret
added theorem wseq.map_think
added theorem wseq.mem_congr
added theorem wseq.mem_cons
added theorem wseq.mem_cons_iff
added theorem wseq.mem_cons_of_mem
added theorem wseq.mem_map
added theorem wseq.mem_of_mem_dropn
added theorem wseq.mem_of_mem_tail
added theorem wseq.mem_rec_on
added theorem wseq.mem_think
added def wseq.nil
added theorem wseq.nil_append
added theorem wseq.not_mem_nil
added def wseq.nth
added theorem wseq.nth_add
added theorem wseq.nth_congr
added theorem wseq.nth_mem
added theorem wseq.nth_of_seq
added theorem wseq.nth_tail
added theorem wseq.nth_terminates_le
added def wseq.of_list
added def wseq.of_list_nil
added def wseq.of_seq
added def wseq.of_stream
added def wseq.productive
added theorem wseq.productive_congr
added def wseq.remove_nth
added def wseq.ret
added theorem wseq.ret_bind
added def wseq.scanl
added theorem wseq.seq_destruct_cons
added theorem wseq.seq_destruct_nil
added def wseq.split_at
added def wseq.tail.aux
added def wseq.tail
added theorem wseq.tail_congr
added theorem wseq.tail_cons
added theorem wseq.tail_nil
added theorem wseq.tail_of_seq
added theorem wseq.tail_think
added def wseq.take
added def wseq.think
added theorem wseq.think_append
added theorem wseq.think_congr
added theorem wseq.think_equiv
added def wseq.to_list
added def wseq.to_list_nil
added theorem wseq.to_list_of_list
added def wseq.to_seq
added theorem wseq.to_seq_of_seq
added def wseq.union
added def wseq.update_nth
added def wseq.zip
added def wseq.zip_with
added def wseq
added theorem set.empty_inter
added theorem set.empty_subset
added theorem set.empty_union
added theorem set.ext
added theorem set.inter_assoc
added theorem set.inter_comm
added theorem set.inter_empty
added theorem set.inter_self
added theorem set.mem_empty_eq
added theorem set.ne_empty_of_mem
added theorem set.not_mem_empty
added theorem set.subset.antisymm
added theorem set.subset.refl
added theorem set.subset.trans
added theorem set.union_assoc
added theorem set.union_comm
added theorem set.union_empty
added theorem set.union_self
added inductive set.finite
added theorem set.finite_image
added theorem set.finite_insert
added theorem set.finite_sUnion
added theorem set.finite_singleton
added theorem set.finite_subset
added theorem set.finite_union
added def set.Inter
added def set.Union
added theorem set.Union_subset
added theorem set.Union_subset_iff
added theorem set.bInter_empty
added theorem set.bInter_insert
added theorem set.bInter_pair
added theorem set.bInter_singleton
added theorem set.bInter_union
added theorem set.bInter_univ
added theorem set.bUnion_empty
added theorem set.bUnion_insert
added theorem set.bUnion_pair
added theorem set.bUnion_singleton
added theorem set.bUnion_subset
added theorem set.bUnion_union
added theorem set.bUnion_univ
added theorem set.compl_Inter
added theorem set.compl_Union
added theorem set.compl_comp_compl
added theorem set.compl_compl
added theorem set.compl_compl_image
added theorem set.compl_empty
added theorem set.compl_eq_univ_diff
added theorem set.compl_inter
added theorem set.compl_inter_self
added theorem set.compl_sInter
added theorem set.compl_sUnion
added theorem set.compl_union
added theorem set.compl_union_self
added theorem set.compl_univ
added theorem set.diff_eq
added theorem set.diff_subset
added def set.disjoint
added theorem set.disjoint_bot_left
added theorem set.disjoint_bot_right
added theorem set.disjoint_symm
added theorem set.empty_ne_univ
added def set.eq_on
added theorem set.eq_sep_of_subset
added theorem set.eq_univ_of_forall
added theorem set.fix_set_compl
added theorem set.image_comp
added theorem set.image_empty
added theorem set.image_id
added theorem set.image_insert_eq
added theorem set.image_subset
added theorem set.image_union
added theorem set.insert_comm
added theorem set.insert_def
added theorem set.insert_eq
added theorem set.insert_eq_of_mem
added theorem set.insert_ne_empty
added theorem set.inter_compl_self
added theorem set.inter_def
added theorem set.inter_distrib_left
added theorem set.inter_left_comm
added theorem set.inter_right_comm
added theorem set.inter_subset_inter
added theorem set.inter_subset_left
added theorem set.inter_subset_right
added theorem set.inter_univ
added theorem set.mem_Inter
added theorem set.mem_Inter_eq
added theorem set.mem_Union_eq
added theorem set.mem_bInter
added theorem set.mem_bUnion
added theorem set.mem_compl
added theorem set.mem_compl_eq
added theorem set.mem_compl_iff
added theorem set.mem_diff
added theorem set.mem_diff_eq
added theorem set.mem_diff_iff
added theorem set.mem_image
added theorem set.mem_image_compl
added theorem set.mem_image_eq
added theorem set.mem_image_of_mem
added theorem set.mem_insert
added theorem set.mem_insert_iff
added theorem set.mem_insert_of_mem
added theorem set.mem_inter
added theorem set.mem_inter_eq
added theorem set.mem_inter_iff
added theorem set.mem_of_mem_diff
added theorem set.mem_powerset
added theorem set.mem_powerset_iff
added theorem set.mem_sInter
added theorem set.mem_sInter_eq
added theorem set.mem_sUnion
added theorem set.mem_sUnion_eq
added theorem set.mem_sep
added theorem set.mem_sep_eq
added theorem set.mem_sep_iff
added theorem set.mem_set_of
added theorem set.mem_set_of_eq
added theorem set.mem_singleton
added theorem set.mem_singleton_iff
added theorem set.mem_union.elim
added theorem set.mem_union_eq
added theorem set.mem_union_iff
added theorem set.mem_union_left
added theorem set.mem_union_right
added theorem set.mem_unionl
added theorem set.mem_unionr
added theorem set.mem_univ
added theorem set.mem_univ_eq
added theorem set.mem_univ_iff
added theorem set.mem_vimage_eq
added theorem set.mono_image
added theorem set.monotone_vimage
added theorem set.nmem_set_of_eq
added theorem set.pair_eq_singleton
added def set.pairwise_on
added def set.sInter
added theorem set.sInter_empty
added theorem set.sInter_image
added theorem set.sInter_insert
added theorem set.sInter_singleton
added theorem set.sInter_union
added theorem set.sUnion_empty
added theorem set.sUnion_image
added theorem set.sUnion_insert
added theorem set.sUnion_singleton
added theorem set.sUnion_subset
added theorem set.sUnion_subset_iff
added theorem set.sUnion_union
added theorem set.sep_subset
added theorem set.set_eq_def
added theorem set.set_of_false
added theorem set.singleton_def
added theorem set.singleton_ne_empty
added theorem set.ssubset_def
added theorem set.ssubset_insert
added theorem set.subset_Inter
added theorem set.subset_bInter
added theorem set.subset_def
added theorem set.subset_empty_iff
added theorem set.subset_insert
added theorem set.subset_inter
added theorem set.subset_sInter
added theorem set.subset_univ
added theorem set.union_compl_self
added theorem set.union_def
added theorem set.union_diff_cancel
added theorem set.union_distrib_left
added theorem set.union_insert_eq
added theorem set.union_left_comm
added theorem set.union_right_comm
added theorem set.union_same_compl
added theorem set.union_sdiff_same
added theorem set.union_subset
added theorem set.union_subset_iff
added theorem set.union_subset_union
added theorem set.univ_def
added theorem set.univ_inter
added def set.vimage
added theorem set.vimage_Union
added theorem set.vimage_comp
added theorem set.vimage_compl
added theorem set.vimage_empty
added theorem set.vimage_id
added theorem set.vimage_image_eq
added theorem set.vimage_inter
added theorem set.vimage_mono
added theorem set.vimage_sUnion
added theorem set.vimage_union
added theorem set.vimage_univ
added def stream.all
added theorem stream.all_def
added def stream.any
added theorem stream.any_def
added def stream.apply
added def stream.approx
added theorem stream.approx_succ
added theorem stream.approx_zero
added theorem stream.bisim_simple
added theorem stream.coinduction
added theorem stream.composition
added def stream.cons
added def stream.const
added theorem stream.const_eq
added def stream.corec'
added theorem stream.corec'_eq
added def stream.corec
added theorem stream.corec_def
added theorem stream.corec_eq
added def stream.corec_on
added def stream.cycle
added theorem stream.cycle_eq
added theorem stream.cycle_singleton
added def stream.drop
added theorem stream.drop_const
added theorem stream.drop_drop
added theorem stream.drop_map
added theorem stream.drop_succ
added theorem stream.drop_zip
added theorem stream.eq_of_bisim
added def stream.even
added theorem stream.even_cons_cons
added theorem stream.even_interleave
added theorem stream.even_tail
added def stream.head
added theorem stream.head_cons
added theorem stream.head_even
added theorem stream.head_iterate
added theorem stream.head_map
added theorem stream.head_zip
added theorem stream.homomorphism
added theorem stream.identity
added def stream.inits
added theorem stream.inits_core_eq
added theorem stream.inits_eq
added theorem stream.inits_tail
added theorem stream.interchange
added theorem stream.interleave_eq
added def stream.iterate
added theorem stream.iterate_eq
added theorem stream.iterate_id
added def stream.map
added theorem stream.map_cons
added theorem stream.map_const
added theorem stream.map_eq
added theorem stream.map_eq_apply
added theorem stream.map_id
added theorem stream.map_iterate
added theorem stream.map_map
added theorem stream.map_tail
added theorem stream.mem_cons
added theorem stream.mem_cons_of_mem
added theorem stream.mem_const
added theorem stream.mem_cycle
added theorem stream.mem_map
added theorem stream.mem_of_mem_even
added theorem stream.mem_of_mem_odd
added theorem stream.mem_of_nth_eq
added def stream.nats
added theorem stream.nats_eq
added def stream.nth
added theorem stream.nth_approx
added theorem stream.nth_const
added theorem stream.nth_drop
added theorem stream.nth_even
added theorem stream.nth_inits
added theorem stream.nth_map
added theorem stream.nth_nats
added theorem stream.nth_odd
added theorem stream.nth_of_bisim
added theorem stream.nth_succ
added theorem stream.nth_tails
added theorem stream.nth_zero_cons
added theorem stream.nth_zip
added def stream.odd
added theorem stream.odd_eq
added def stream.pure
added def stream.tail
added theorem stream.tail_cons
added theorem stream.tail_const
added theorem stream.tail_drop
added theorem stream.tail_eq_drop
added theorem stream.tail_even
added theorem stream.tail_inits
added theorem stream.tail_interleave
added theorem stream.tail_iterate
added theorem stream.tail_map
added theorem stream.tail_zip
added def stream.tails
added theorem stream.tails_eq
added theorem stream.take_lemma
added def stream.unfolds
added theorem stream.unfolds_eq
added theorem stream.unfolds_head_eq
added def stream.zip
added theorem stream.zip_eq
added theorem stream.zip_inits_tails
added def stream
added def vector.append
added def vector.cons
added theorem vector.cons_head_tail
added def vector.drop
added def vector.elim
added def vector.head
added theorem vector.head_cons
added def vector.length
added def vector.map
added theorem vector.map_cons
added theorem vector.map_nil
added def vector.map₂
added def vector.nil
added def vector.nth
added def vector.of_fn
added def vector.repeat
added def vector.tail
added theorem vector.tail_cons
added def vector.take
added def vector.to_list
added theorem vector.to_list_append
added theorem vector.to_list_cons
added theorem vector.to_list_drop
added theorem vector.to_list_length
added theorem vector.to_list_mk
added theorem vector.to_list_nil
added theorem vector.to_list_take
added def vector
added theorem and_distrib
added theorem and_distrib_right
added theorem and_iff_not_or_not
added theorem and_imp_iff
added theorem and_implies_left
added theorem and_implies_right
added theorem and_not_of_not_implies
added theorem and_not_self_iff
added theorem and_of_and_of_imp_left
added theorem bexists.elim
added theorem bexists.intro
added theorem bexists_congr
added theorem bexists_of_bexists
added theorem bexists_of_exists
added theorem bexists_or_distrib
added theorem bforall_and_distrib
added theorem bforall_congr
added theorem bforall_of_bforall
added theorem bforall_of_forall
added theorem bforall_true_iff
added theorem by_contradiction
added theorem dec_em
added theorem eq_iff_le_and_le
added theorem exists_implies_distrib
added theorem exists_of_bexists
added theorem exists_of_exists
added theorem exists_or_distrib
added theorem exists_p_iff_p
added theorem exists_prop_iff
added theorem forall_and_distrib
added theorem forall_eq
added theorem forall_of_bforall
added theorem forall_of_forall
added theorem forall_or_distrib_left
added theorem forall_p_iff_p
added theorem forall_true_iff
added theorem implies_false_iff
added theorem implies_iff
added theorem implies_iff_not_or
added theorem implies_intro
added theorem implies_of_not_or
added theorem implies_self
added theorem not_and_iff
added theorem not_and_not_of_not_or
added theorem not_and_of_not_left
added theorem not_and_of_not_or_not
added theorem not_and_of_not_right
added theorem not_and_self_iff
added theorem not_exists_iff
added theorem not_forall_iff
added theorem not_imp_iff_not_imp
added theorem not_implies_iff
added theorem not_implies_of_and_not
added theorem not_not_elim
added theorem not_not_iff
added theorem not_not_of_not_implies
added theorem not_of_not_implies
added theorem not_or_iff
added theorem not_or_not_of_not_and'
added theorem not_or_not_of_not_and
added theorem not_or_of_implies
added theorem not_or_of_not_and_not
added theorem of_not_implies
added theorem or.elim3
added theorem or_distrib
added theorem or_distrib_right
added theorem or_iff_not_and_not
added theorem or_iff_or
added theorem or_imp_iff_and_imp
added theorem or_implies_distrib
added theorem or_of_not_implies'
added theorem or_of_not_implies
added theorem or_resolve_left
added theorem or_resolve_right
added theorem peirce'
added theorem peirce
added theorem prod.exists
added theorem prod.forall
added theorem prod.mk.inj_iff
added theorem set_of_subset_set_of
added theorem {u}
added theorem nat.shiftl_succ
added theorem nat.shiftl_zero
added def Class.Union
added theorem Class.Union_hom
added theorem Class.diff_hom
added theorem Class.empty_hom
added def Class.fval
added theorem Class.fval_ex
added theorem Class.insert_hom
added theorem Class.inter_hom
added def Class.iota
added theorem Class.iota_ex
added theorem Class.iota_val
added theorem Class.mem_hom_left
added theorem Class.mem_hom_right
added theorem Class.mem_univ
added theorem Class.of_Set.inj
added def Class.of_Set
added def Class.powerset
added theorem Class.powerset_hom
added theorem Class.sep_hom
added theorem Class.subset_hom
added def Class.to_Set
added theorem Class.to_Set_of_Set
added theorem Class.union_hom
added def Class.univ
added def Class
added def Set.Union
added theorem Set.Union_lem
added theorem Set.Union_singleton
added def Set.choice_mem
added def Set.empty
added def Set.eq_empty
added def Set.ext
added def Set.ext_iff
added def Set.funs
added def Set.image.mk
added def Set.image
added theorem Set.induction_on
added def Set.is_func
added def Set.map_fval
added theorem Set.map_is_func
added theorem Set.map_unique
added def Set.mem
added theorem Set.mem_Union
added theorem Set.mem_diff
added def Set.mem_empty
added def Set.mem_funs
added def Set.mem_image
added def Set.mem_insert
added theorem Set.mem_inter
added theorem Set.mem_map
added theorem Set.mem_pair
added theorem Set.mem_pair_sep
added theorem Set.mem_powerset
added def Set.mem_prod
added theorem Set.mem_sep
added theorem Set.mem_singleton'
added theorem Set.mem_singleton
added theorem Set.mem_union
added def Set.omega
added theorem Set.omega_succ
added theorem Set.omega_zero
added def Set.pair
added def Set.pair_inj
added def Set.pair_sep
added def Set.powerset
added def Set.prod
added theorem Set.regularity
added theorem Set.singleton_inj
added theorem Set.subset_iff
added def Set.to_set
added def Set
added def arity
added def pSet.Union
added def pSet.arity.equiv
added inductive pSet.definable
added def pSet.embed
added def pSet.equiv.eq
added def pSet.equiv.euc
added def pSet.equiv.ext
added def pSet.equiv.refl
added def pSet.equiv.symm
added def pSet.equiv.trans
added def pSet.equiv
added def pSet.func
added def pSet.image
added def pSet.mem.ext
added def pSet.mem.mk
added def pSet.mem
added theorem pSet.mem_Union
added def pSet.mem_empty
added def pSet.mem_image
added theorem pSet.mem_powerset
added def pSet.of_nat
added def pSet.omega
added def pSet.powerset
added def pSet.resp.equiv
added def pSet.resp.euc
added def pSet.resp.eval
added def pSet.resp.f
added def pSet.resp.refl
added def pSet.resp
added def pSet.to_set
added def pSet.type
added inductive pSet
added theorem set.compl_comp_compl
added theorem set.compl_compl
added theorem set.compl_compl_image
added theorem set.compl_empty
added theorem set.compl_eq_univ_diff
added theorem set.compl_inter
added theorem set.compl_inter_self
added theorem set.compl_union
added theorem set.compl_union_self
added theorem set.compl_univ
added theorem set.diff_eq
added theorem set.diff_subset
added theorem set.empty_def
added theorem set.empty_ne_univ
added def set.eq_on
added theorem set.eq_sep_of_subset
added theorem set.eq_univ_of_forall
added theorem set.fix_set_compl
added theorem set.image_comp
added theorem set.image_empty
added theorem set.image_id
added theorem set.image_insert_eq
added theorem set.image_subset
added theorem set.image_union
added theorem set.insert_comm
added theorem set.insert_def
added theorem set.insert_eq
added theorem set.insert_eq_of_mem
added theorem set.insert_ne_empty
added theorem set.inter_compl_self
added theorem set.inter_def
added theorem set.inter_distrib_left
added theorem set.inter_left_comm
added theorem set.inter_right_comm
added theorem set.inter_subset_left
added theorem set.inter_subset_right
added theorem set.inter_univ
added theorem set.mem_compl
added theorem set.mem_compl_eq
added theorem set.mem_compl_iff
added theorem set.mem_diff
added theorem set.mem_diff_eq
added theorem set.mem_diff_iff
added theorem set.mem_image
added theorem set.mem_image_compl
added theorem set.mem_image_eq
added theorem set.mem_image_of_mem
added theorem set.mem_insert
added theorem set.mem_insert_iff
added theorem set.mem_insert_of_mem
added theorem set.mem_inter
added theorem set.mem_inter_eq
added theorem set.mem_inter_iff
added theorem set.mem_of_mem_diff
added theorem set.mem_powerset
added theorem set.mem_powerset_iff
added theorem set.mem_sep
added theorem set.mem_sep_eq
added theorem set.mem_sep_iff
added theorem set.mem_set_of
added theorem set.mem_singleton
added theorem set.mem_singleton_iff
added theorem set.mem_union.elim
added theorem set.mem_union_eq
added theorem set.mem_union_iff
added theorem set.mem_union_left
added theorem set.mem_union_right
added theorem set.mem_unionl
added theorem set.mem_unionr
added theorem set.mem_univ
added theorem set.mem_univ_eq
added theorem set.mem_univ_iff
added theorem set.pair_eq_singleton
added theorem set.sep_subset
added theorem set.set_eq_def
added theorem set.singleton_def
added theorem set.singleton_ne_empty
added theorem set.subset_def
added theorem set.subset_empty_iff
added theorem set.subset_insert
added theorem set.subset_inter
added theorem set.subset_univ
added theorem set.union_compl_self
added theorem set.union_def
added theorem set.union_diff_cancel
added theorem set.union_distrib_left
added theorem set.union_left_comm
added theorem set.union_right_comm
added theorem set.union_subset
added theorem set.univ_def
added theorem set.univ_inter
added theorem NoMember
added inductive and3
added inductive or3
added theorem foo:
added structure auto.auto_config
added inductive auto.case_option
added theorem auto.not_and_eq
added theorem auto.not_exists_eq
added theorem auto.not_forall_eq
added theorem auto.not_implies_eq
added theorem auto.not_not_eq
added theorem auto.not_or_eq
added theorem curry_iff
added theorem iff_def
added theorem implies_and_iff
added theorem {u}
added theorem Inf_image
added theorem Sup_image
added theorem mem_image
added theorem {u
added def form_of_string
added def parser.apply
added def parser.chainl1
added def parser.chainl
added def parser.chainr1
added def parser.chainr
added def parser.item
added def parser.many1
added def parser.many
added def parser.many_aux
added def parser.parse
added def parser.sat
added def parser.sepby1
added def parser.sepby
added def parser.space
added def parser.symb
added def parser.take_char
added def parser.token
added def parser
added def parser_bind
added def parser_fmap
added def parser_pure
added theorem {u
added theorem {u}
added theorem inter_def
added theorem mem_set_of
added def my_id
added def my_id_def
added theorem subset_def
added theorem subset_inter
added theorem union_def
added theorem union_subset
added theorem classical.cases
added theorem closure_prod_eq
added theorem compact_pi_infinite
added def continuous
added theorem continuous_Inf_dom
added theorem continuous_Inf_rng
added theorem continuous_Prop
added theorem continuous_bot
added theorem continuous_compose
added theorem continuous_fst
added theorem continuous_id
added theorem continuous_iff_towards
added theorem continuous_induced_dom
added theorem continuous_induced_rng
added theorem continuous_inf_dom
added theorem continuous_infi_dom
added theorem continuous_infi_rng
added theorem continuous_inl
added theorem continuous_inr
added theorem continuous_prod_mk
added theorem continuous_snd
added theorem continuous_subtype_mk
added theorem continuous_subtype_val
added theorem continuous_sum_rec
added theorem continuous_sup_rng
added theorem continuous_top
added theorem false_neq_true
added theorem map_nhds_induced_eq
added theorem nhds_induced_eq_vmap
added theorem nhds_pi
added theorem nhds_prod_eq
added theorem open_induced
added theorem open_set_prod
added theorem open_singleton_true
added theorem prod_eq_generate_from
added theorem subtype.val_image
added theorem univ_eq_true_false
added def closed
added theorem closed_Inter
added theorem closed_closure
added theorem closed_compl_iff_open
added theorem closed_empty
added theorem closed_iff_nhds
added theorem closed_sInter
added theorem closed_union
added theorem closed_univ
added def closure
added theorem closure_closure
added theorem closure_compl_eq
added theorem closure_empty
added theorem closure_eq_iff_closed
added theorem closure_eq_nhds
added theorem closure_eq_of_closed
added theorem closure_minimal
added theorem closure_mono
added theorem closure_union
added theorem closure_univ
added def compact
added theorem eq_of_nhds_eq_nhds
added theorem eq_of_nhds_neq_bot
added theorem generate_from_le
added def interior
added theorem interior_compl_eq
added theorem interior_empty
added theorem interior_eq_iff_open
added theorem interior_eq_nhds
added theorem interior_eq_of_open
added theorem interior_inter
added theorem interior_interior
added theorem interior_maximal
added theorem interior_mono
added theorem interior_subset
added theorem interior_univ
added theorem le_of_nhds_le_nhds
added def locally_finite
added theorem map_nhds
added theorem mem_nhds_sets
added theorem mem_nhds_sets_iff
added def nhds
added theorem nhds_mono
added theorem nhds_neq_bot
added theorem nhds_sets
added theorem nhds_supr
added def open'
added theorem open_Union
added theorem open_compl_iff_closed
added theorem open_diff
added theorem open_empty
added theorem open_iff_nhds
added theorem open_inter
added theorem open_interior
added theorem open_sUnion
added theorem open_univ
added theorem return_le_nhds
added theorem subset_closure
added theorem sup_eq_generate_from
added theorem supr_eq_generate_from
added theorem t2_space_top
added structure topological_space
added theorem topological_space_eq
added def Cauchy.gen
added theorem Cauchy.monotone_gen
added def Cauchy
added def cauchy
added theorem cauchy_downwards
added theorem cauchy_map
added theorem cauchy_nhds
added theorem cauchy_pure
added theorem cauchy_vmap
added theorem comp_le_uniformity3
added theorem comp_le_uniformity
added def comp_rel
added theorem complete_of_closed
added theorem continuous_of_uniform
added theorem id_comp_rel
added def id_rel
added theorem le_nhds_of_cauchy_adhp
added theorem lift_nhds_left
added theorem lift_nhds_right
added theorem mem_nhds_left
added theorem mem_nhds_right
added theorem monotone_comp_rel
added theorem nhds_eq_uniformity
added theorem prod_mk_mem_comp_rel
added theorem refl_le_uniformity
added theorem refl_mem_uniformity
added def separated
added theorem separated_equiv
added theorem supr_uniformity
added theorem swap_id_rel
added theorem symm_le_uniformity
added theorem symm_of_uniformity
added def totally_bounded
added theorem uniform_space_eq
added def uniformity
added theorem uniformity_eq_symm
added theorem uniformity_le_symm
added theorem uniformly_extend_spec