E
Efficient_Rec.R [variable, in R]
Efficient_Rec [section, in Efficient_Rec]
Efficient_Rec.R_wf [variable, in R_wf]
elim [projection, in elim]
elim_type [projection, in elim_type]
Elts [section, in Elts]
Elts.A [variable, in A]
Elts.eq_dec [variable, in eq_dec]
EmptyBag [definition, in EmptyBag]
Emptyset [definition, in Emptyset]
EmptyString [constructor, in EmptyString]
Empty_set_zero [lemma, in Empty_set_zero]
empty_set [definition, in empty_set]
Empty_set_zero' [lemma, in Empty_set_zero']
Empty_set [inductive, in Empty_set]
Empty_set [inductive, in Empty_set]
Empty_set_is_Bottom [lemma, in Empty_set_is_Bottom]
Empty_set_minimal [lemma, in Empty_set_minimal]
Empty_is_finite [constructor, in Empty_is_finite]
ENCODING_VALUE [section, in ENCODING_VALUE]
Ensemble [definition, in Ensemble]
Ensembles [section, in Ensembles]
Ensembles [library]
Ensembles_finis_facts.U [variable, in U]
Ensembles_finis.U [variable, in U]
Ensembles_facts.U [variable, in U]
Ensembles_classical.U [variable, in U]
Ensembles_finis_facts [section, in Ensembles_finis_facts]
Ensembles_facts [section, in Ensembles_facts]
Ensembles_finis [section, in Ensembles_finis]
Ensembles_classical [section, in Ensembles_classical]
Ensembles.U [variable, in U]
eps [abbreviation, in eps]
epsilon [definition, in epsilon]
epsilon [definition, in epsilon]
Epsilon [library]
EpsilonStatement [abbreviation, in EpsilonStatement]
EpsilonStatement_on [definition, in EpsilonStatement_on]
epsilon_imp_small_drinker [lemma, in epsilon_imp_small_drinker]
epsilon_inh_irrelevance [lemma, in epsilon_inh_irrelevance]
epsilon_imp_constructive_indefinite_description [lemma, in epsilon_imp_constructive_indefinite_description]
epsilon_spec [definition, in epsilon_spec]
epsilon_spec [definition, in epsilon_spec]
epsilon_statement [axiom, in epsilon_statement]
eps2 [lemma, in eps2]
eps2_Rgt_R0 [lemma, in eps2_Rgt_R0]
eps4 [lemma, in eps4]
Eq [module, in Eq]
Eq [constructor, in Eq]
EQ [constructor, in EQ]
eq [inductive, in eq]
eqb [definition, in eqb]
EqbNotation [module, in EqbNotation]
_ =? _ [notation, in ::x_'=?'_x]
EqbSpec [module, in EqbSpec]
EqbSpec.eqb_eq [axiom, in eqb_eq]
eqb_refl [lemma, in eqb_refl]
eqb_false_iff [lemma, in eqb_false_iff]
eqb_prop [lemma, in eqb_prop]
eqb_true_iff [lemma, in eqb_true_iff]
eqb_eq [lemma, in eqb_eq]
eqb_negb2 [lemma, in eqb_negb2]
eqb_reflx [lemma, in eqb_reflx]
eqb_negb1 [lemma, in eqb_negb1]
eqb_subst [lemma, in eqb_subst]
eqb31 [definition, in eqb31]
eqb31_eq [lemma, in eqb31_eq]
eqb31_correct [lemma, in eqb31_correct]
EqDec [record, in EqDec]
EqDec [inductive, in EqDec]
EqDec [record, in EqDec]
EqDec [inductive, in EqDec]
Eqdep [library]
EqdepDec [section, in EqdepDec]
EqdepDec.A [variable, in A]
EqdepDec.comp [variable, in comp]
EqdepDec.eq_dec [variable, in eq_dec]
EqdepDec.nu [variable, in nu]
EqdepDec.nu_inv [variable, in nu_inv]
EqdepDec.nu_constant [variable, in nu_constant]
EqdepDec.proj [variable, in proj]
EqdepDec.x [variable, in x]
EqdepElimination [module, in EqdepElimination]
EqdepElimination.eq_rect_eq [axiom, in eq_rect_eq]
EqdepFacts [library]
EqdepTheory [module, in EqdepTheory]
EqdepTheory [module, in EqdepTheory]
EqdepTheory [module, in EqdepTheory]
EqdepTheory.Axioms [section, in Axioms]
EqdepTheory.Axioms.U [variable, in U]
EqdepTheory.eq_rec_eq [lemma, in eq_rec_eq]
EqdepTheory.eq_rect_eq [lemma, in eq_rect_eq]
EqdepTheory.eq_dep_eq [lemma, in eq_dep_eq]
EqdepTheory.inj_pair2 [lemma, in inj_pair2]
EqdepTheory.inj_pairT2 [abbreviation, in inj_pairT2]
EqdepTheory.Streicher_K [lemma, in Streicher_K]
EqdepTheory.UIP [lemma, in UIP]
EqdepTheory.UIP_refl [lemma, in UIP_refl]
Eqdep_dec [library]
eqf [definition, in eqf]
eqf_equiv [instance, in eqf_equiv]
EqLe [module, in EqLe]
EqLeNotation [module, in EqLeNotation]
EqLe' [module, in EqLe']
eqlistA [inductive, in eqlistA]
eqlistA_rev_app [lemma, in eqlistA_rev_app]
eqlistA_length [lemma, in eqlistA_length]
eqlistA_altdef [lemma, in eqlistA_altdef]
eqlistA_cons [constructor, in eqlistA_cons]
eqlistA_equiv [instance, in eqlistA_equiv]
eqlistA_app [lemma, in eqlistA_app]
eqlistA_nil [constructor, in eqlistA_nil]
eqlistA_rev [lemma, in eqlistA_rev]
eqlistA_equivlistA [instance, in eqlistA_equivlistA]
EqLt [module, in EqLt]
EqLtLe [module, in EqLtLe]
EqLtLeNotation [module, in EqLtLeNotation]
EqLtLe' [module, in EqLtLe']
EqLtNotation [module, in EqLtNotation]
EqLt' [module, in EqLt']
eqm [definition, in eqm]
eqm_setoid [instance, in eqm_setoid]
eqm_refl [lemma, in eqm_refl]
eqm_trans [lemma, in eqm_trans]
eqm_sym [lemma, in eqm_sym]
EqNat [library]
EqNotation [module, in EqNotation]
EqNotations [module, in EqNotations]
rew _ in _ [notation, in ::'rew'_x_'in'_x]
rew <- _ in _ [notation, in ::'rew'_'<-'_x_'in'_x]
rew -> _ in _ [notation, in ::'rew'_'->'_x_'in'_x]
_ ~= _ [notation, in ::x_'~='_x]
_ == _ [notation, in ::x_'=='_x]
EqProperties [module, in EqProperties]
EqProperties [module, in EqProperties]
eqR_Qeq [lemma, in eqR_Qeq]
EqShiftL [definition, in EqShiftL]
EqShiftL_size [lemma, in EqShiftL_size]
EqShiftL_firstr [lemma, in EqShiftL_firstr]
EqShiftL_incr [lemma, in EqShiftL_incr]
EqShiftL_shiftr [lemma, in EqShiftL_shiftr]
EqShiftL_le [lemma, in EqShiftL_le]
EqShiftL_i2l [lemma, in EqShiftL_i2l]
EqShiftL_twice_plus_one [lemma, in EqShiftL_twice_plus_one]
EqShiftL_zero [lemma, in EqShiftL_zero]
EqShiftL_twice [lemma, in EqShiftL_twice]
EqShiftL_incrbis [lemma, in EqShiftL_incrbis]
eqst [constructor, in eqst]
EqSt [inductive, in EqSt]
EqSt_reflex [lemma, in EqSt_reflex]
eqst_ntheq [lemma, in eqst_ntheq]
Equalities [library]
EqualitiesFacts [library]
Equality [library]
EqualityModulo [section, in EqualityModulo]
EqualityModulo.N [variable, in N]
_ == _ [notation, in ::x_'=='_x]
EqualityType [module, in EqualityType]
EqualityType [module, in EqualityType]
EqualityTypeBoth [module, in EqualityTypeBoth]
EqualityTypeBoth' [module, in EqualityTypeBoth']
EqualityTypeOrig [module, in EqualityTypeOrig]
EqualityTypeOrig' [module, in EqualityTypeOrig']
EqualityType' [module, in EqualityType']
equal_f [lemma, in equal_f]
equiv [projection, in equiv]
equiv [definition, in equiv]
equiv [definition, in equiv]
equivalence [record, in equivalence]
Equivalence [record, in Equivalence]
Equivalence [inductive, in Equivalence]
Equivalence [section, in Equivalence]
Equivalence [library]
Equivalences [section, in Equivalences]
Equivalences.U [variable, in U]
Equivalence_Reflexive [projection, in Equivalence_Reflexive]
Equivalence_PER [instance, in Equivalence_PER]
Equivalence_Symmetric [projection, in Equivalence_Symmetric]
Equivalence_Transitive [projection, in Equivalence_Transitive]
equivalence_default [instance, in equivalence_default]
equivalence_rewrite_relation [instance, in equivalence_rewrite_relation]
EquivDec [library]
equivlistA [definition, in equivlistA]
equivlistA_app_proper [instance, in equivlistA_app_proper]
equivlistA_NoDupA_split [lemma, in equivlistA_NoDupA_split]
equivlistA_app_idem [lemma, in equivlistA_app_idem]
equivlistA_permute_heads [lemma, in equivlistA_permute_heads]
equivlistA_cons_nil [lemma, in equivlistA_cons_nil]
equivlistA_nil_eq [lemma, in equivlistA_nil_eq]
equivlistA_double_head [lemma, in equivlistA_double_head]
equivlistA_cons_proper [instance, in equivlistA_cons_proper]
equivlist_equiv [instance, in equivlist_equiv]
equiv_reflexive [instance, in equiv_reflexive]
equiv_decb [definition, in equiv_decb]
equiv_decb [definition, in equiv_decb]
equiv_sym [projection, in equiv_sym]
equiv_Tree [definition, in equiv_Tree]
equiv_symmetric [instance, in equiv_symmetric]
Equiv_from_preorder [lemma, in Equiv_from_preorder]
equiv_refl [projection, in equiv_refl]
equiv_trans [projection, in equiv_trans]
Equiv_from_order [lemma, in Equiv_from_order]
equiv_dec [projection, in equiv_dec]
equiv_dec [constructor, in equiv_dec]
equiv_dec [projection, in equiv_dec]
equiv_dec [constructor, in equiv_dec]
equiv_eqex_eqdep [abbreviation, in equiv_eqex_eqdep]
equiv_nequiv_trans [lemma, in equiv_nequiv_trans]
equiv_transitive [instance, in equiv_transitive]
eq_proofs_unicity [lemma, in eq_proofs_unicity]
eq_refl [constructor, in eq_refl]
eq_dep1_intro [constructor, in eq_dep1_intro]
eq_IZR [lemma, in eq_IZR]
eq_bool_prop_intro [lemma, in eq_bool_prop_intro]
eq_rect_eq__eq_dep1_eq [lemma, in eq_rect_eq__eq_dep1_eq]
eq_dep_strictly_stronger_JMeq [lemma, in eq_dep_strictly_stronger_JMeq]
eq_dep_trans [lemma, in eq_dep_trans]
eq_nat_is_eq [lemma, in eq_nat_is_eq]
eq_add_S [definition, in eq_add_S]
eq_true_iff_eq [lemma, in eq_true_iff_eq]
eq_dep_id_JMeq [lemma, in eq_dep_id_JMeq]
eq_dep1 [inductive, in eq_dep1]
eq_dep_eq_dec [lemma, in eq_dep_eq_dec]
eq_Symmetric [instance, in eq_Symmetric]
eq_dep [inductive, in eq_dep]
eq_nat_decide [lemma, in eq_nat_decide]
eq_dep_eq__inj_pairT2 [abbreviation, in eq_dep_eq__inj_pairT2]
eq_equivalence [instance, in eq_equivalence]
eq_dep_eq_positive [abbreviation, in eq_dep_eq_positive]
eq_sigT_fst [lemma, in eq_sigT_fst]
eq_true [inductive, in eq_true]
eq_sigS_eq_dep [abbreviation, in eq_sigS_eq_dep]
eq_true_ind_r [lemma, in eq_true_ind_r]
eq_sigT_eq_dep [lemma, in eq_sigT_eq_dep]
eq_sigT_snd [lemma, in eq_sigT_snd]
eq_nat_refl [lemma, in eq_nat_refl]
eq_dep_refl [lemma, in eq_dep_refl]
eq_dep_eq_sigT [lemma, in eq_dep_eq_sigT]
eq_sigT_sig_eq [lemma, in eq_sigT_sig_eq]
Eq_rect_eq.eq_rect_eq [axiom, in eq_rect_eq]
Eq_rect_eq.eq_rect_eq [lemma, in eq_rect_eq]
eq_setoid [instance, in eq_setoid]
eq_rec_r [definition, in eq_rec_r]
eq_nat_elim [lemma, in eq_nat_elim]
eq_Transitive [instance, in eq_Transitive]
eq_true_rect_r [lemma, in eq_true_rect_r]
eq_sig_fst [lemma, in eq_sig_fst]
eq_dep_JMeq [lemma, in eq_dep_JMeq]
eq_dep_eq_sig [lemma, in eq_dep_eq_sig]
eq_sym [lemma, in eq_sym]
eq_bool_prop_elim [lemma, in eq_bool_prop_elim]
eq_dep1_dep [lemma, in eq_dep1_dep]
eq_sig_snd [lemma, in eq_sig_snd]
eq_sigT_iff_eq_dep [lemma, in eq_sigT_iff_eq_dep]
eq_Fix_F_sub [lemma, in eq_Fix_F_sub]
eq_nat_eq [lemma, in eq_nat_eq]
eq_Dom [definition, in eq_Dom]
eq_rect_eq_dec [lemma, in eq_rect_eq_dec]
eq_iff_eq_true [lemma, in eq_iff_eq_true]
eq_rect_r [definition, in eq_rect_r]
eq_rect_eq__eq_dep_eq [lemma, in eq_rect_eq__eq_dep_eq]
eq_dep_sym [lemma, in eq_dep_sym]
eq_Reflexive [instance, in eq_Reflexive]
eq_nat_dec [lemma, in eq_nat_dec]
eq_nth_iff [lemma, in eq_nth_iff]
eq_dep_eq__inj_pair2 [lemma, in eq_dep_eq__inj_pair2]
eq_trans [lemma, in eq_trans]
eq_nat [definition, in eq_nat]
eq_true_false_abs [lemma, in eq_true_false_abs]
eq_proper_proxy [lemma, in eq_proper_proxy]
eq_dec [definition, in eq_dec]
eq_true_rec_r [lemma, in eq_true_rec_r]
Eq_dep_eq [definition, in Eq_dep_eq]
Eq_rect_eq [module, in Eq_rect_eq]
Eq_rect_eq [definition, in Eq_rect_eq]
Eq_rect_eq [module, in Eq_rect_eq]
eq_dep_eq__UIP [lemma, in eq_dep_eq__UIP]
eq_dep_dep1 [lemma, in eq_dep_dep1]
eq_stepl [lemma, in eq_stepl]
eq_subrelation [lemma, in eq_subrelation]
eq_sig_eq_dep [lemma, in eq_sig_eq_dep]
eq_S [definition, in eq_S]
eq_dep_intro [constructor, in eq_dep_intro]
eq_indd [definition, in eq_indd]
eq_indd [definition, in eq_indd]
eq_eq_nat [lemma, in eq_eq_nat]
eq_sig_iff_eq_dep [lemma, in eq_sig_iff_eq_dep]
eq_IZR_R0 [lemma, in eq_IZR_R0]
eq_ind_r [definition, in eq_ind_r]
eq_true_not_negb [lemma, in eq_true_not_negb]
eq_true_negb_classical [lemma, in eq_true_negb_classical]
Eq' [module, in Eq']
eq0 [definition, in eq0]
error [definition, in error]
eta_expansion_dep [lemma, in eta_expansion_dep]
eta_expansion [lemma, in eta_expansion]
euclid [lemma, in euclid]
Euclid [inductive, in Euclid]
Euclid [library]
euclidian_division [lemma, in euclidian_division]
EuclidSpec [module, in EuclidSpec]
EuclidSpec.mod_always_pos [axiom, in mod_always_pos]
Euclid_intro [constructor, in Euclid_intro]
euclid_rec [lemma, in euclid_rec]
eucl_dev [lemma, in eucl_dev]
euler [definition, in euler]
EUn [definition, in EUn]
EUn_noempty [lemma, in EUn_noempty]
Even [definition, in Even]
even [definition, in even]
even [inductive, in even]
Even [library]
eventually [definition, in eventually]
event_O [lemma, in event_O]
even_mult_aux [lemma, in even_mult_aux]
even_plus_aux [lemma, in even_plus_aux]
even_plus_even_inv_l [lemma, in even_plus_even_inv_l]
Even_equiv [lemma, in Even_equiv]
even_plus_odd_inv_r [lemma, in even_plus_odd_inv_r]
even_mult_inv_l [lemma, in even_mult_inv_l]
even_mult_l [lemma, in even_mult_l]
even_plus_split [lemma, in even_plus_split]
even_div2 [lemma, in even_div2]
even_odd_cor [lemma, in even_odd_cor]
even_O [constructor, in even_O]
even_S [constructor, in even_S]
even_odd_double [lemma, in even_odd_double]
even_even_plus [lemma, in even_even_plus]
even_mult_inv_r [lemma, in even_mult_inv_r]
even_spec [lemma, in even_spec]
even_or_odd [lemma, in even_or_odd]
even_mult_r [lemma, in even_mult_r]
even_2n [lemma, in even_2n]
even_plus_odd_inv_l [lemma, in even_plus_odd_inv_l]
even_odd_div2 [lemma, in even_odd_div2]
even_plus_even_inv_r [lemma, in even_plus_even_inv_r]
even_odd_dec [lemma, in even_odd_dec]
even_double [lemma, in even_double]
ex [inductive, in ex]
Examples [section, in Examples]
Examples.ex1 [variable, in ex1]
Examples.ex10 [variable, in ex10]
Examples.ex2 [variable, in ex2]
Examples.ex3 [variable, in ex3]
Examples.ex4 [variable, in ex4]
Examples.ex5 [variable, in ex5]
Examples.ex6 [variable, in ex6]
Examples.ex7 [variable, in ex7]
Examples.ex8 [variable, in ex8]
Examples.ex9 [variable, in ex9]
Exc [definition, in Exc]
except [definition, in except]
excluded_middle_Godel_Dummett [lemma, in excluded_middle_Godel_Dummett]
excluded_middle_informative [lemma, in excluded_middle_informative]
excluded_middle_informative [lemma, in excluded_middle_informative]
excluded_middle_independence_general_premises [lemma, in excluded_middle_independence_general_premises]
excluded_middle [definition, in excluded_middle]
exist [constructor, in exist]
existS [abbreviation, in existS]
Exists [inductive, in Exists]
Exists [inductive, in Exists]
Exists [inductive, in Exists]
existsb [definition, in existsb]
existsb_app [lemma, in existsb_app]
existsb_exists [lemma, in existsb_exists]
existsb_nth [lemma, in existsb_nth]
Exists_nil [lemma, in Exists_nil]
Exists_cons_hd [constructor, in Exists_cons_hd]
Exists_cons_hd [constructor, in Exists_cons_hd]
exists_last [lemma, in exists_last]
Exists_cons_tl [constructor, in Exists_cons_tl]
Exists_cons_tl [constructor, in Exists_cons_tl]
Exists_cons [lemma, in Exists_cons]
exists_le [constructor, in exists_le]
Exists_exists [lemma, in Exists_exists]
exists_lt [lemma, in exists_lt]
exists_S [constructor, in exists_S]
exists_S_le [lemma, in exists_S_le]
exists_in_int [lemma, in exists_in_int]
exists_between [inductive, in exists_between]
exists_inhabited [lemma, in exists_inhabited]
exists_beq_eq [definition, in exists_beq_eq]
exists_atan_in_frame [lemma, in exists_atan_in_frame]
exists_le_S [lemma, in exists_le_S]
Exists_map [lemma, in Exists_map]
Exists2 [inductive, in Exists2]
existS2 [abbreviation, in existS2]
Exists2_cons_hd [constructor, in Exists2_cons_hd]
Exists2_cons_tl [constructor, in Exists2_cons_tl]
existT [constructor, in existT]
existT2 [constructor, in existT2]
exist_exp0 [lemma, in exist_exp0]
exist_cos [lemma, in exist_cos]
exist_exp [lemma, in exist_exp]
exist_sin [lemma, in exist_sin]
exist_PI [lemma, in exist_PI]
exist_cos0 [lemma, in exist_cos0]
exist2 [constructor, in exist2]
exp [definition, in exp]
exp_in [definition, in exp_in]
exp_ln [lemma, in exp_ln]
exp_ineq1 [lemma, in exp_ineq1]
exp_increasing [lemma, in exp_increasing]
exp_le_3 [lemma, in exp_le_3]
exp_plus [lemma, in exp_plus]
exp_Ropp [lemma, in exp_Ropp]
exp_form [lemma, in exp_form]
exp_0 [lemma, in exp_0]
exp_cof_no_R0 [lemma, in exp_cof_no_R0]
exp_lt_inv [lemma, in exp_lt_inv]
exp_inv [lemma, in exp_inv]
exp_pos [lemma, in exp_pos]
exp_pos_pos [lemma, in exp_pos_pos]
Exp_prop [library]
extend [definition, in extend]
extend [definition, in extend]
extended_euclid_algorithm.a [variable, in a]
extended_euclid_algorithm.b [variable, in b]
extended_euclid_algorithm [section, in extended_euclid_algorithm]
ExtendMax [section, in ExtendMax]
ExtendMax.m [variable, in m]
ExtendMax.v [variable, in v]
ExtendMax.w [variable, in w]
extend_tr [definition, in extend_tr]
extend_aux [definition, in extend_aux]
Extension [lemma, in Extension]
ExtensionalEpsilon_imp_EM.epsilon [variable, in epsilon]
ExtensionalEpsilon_imp_EM.epsilon_extensionality [variable, in epsilon_extensionality]
ExtensionalEpsilon_imp_EM.epsilon_spec [variable, in epsilon_spec]
ExtensionalEpsilon_imp_EM [section, in ExtensionalEpsilon_imp_EM]
Extensionality_Ensembles [axiom, in Extensionality_Ensembles]
extensional_epsilon_imp_EM [lemma, in extensional_epsilon_imp_EM]
ext_prop_dep_proof_irrel_cic [lemma, in ext_prop_dep_proof_irrel_cic]
ext_prop_dep_proof_irrel_cc [lemma, in ext_prop_dep_proof_irrel_cc]
ext_prop_fixpoint [lemma, in ext_prop_fixpoint]
ext_prop_dep_proof_irrel_gen [lemma, in ext_prop_dep_proof_irrel_gen]
ex_impl_morphism [instance, in ex_impl_morphism]
ex_intro [constructor, in ex_intro]
ex_not_not_all [lemma, in ex_not_not_all]
ex_not_not_all [lemma, in ex_not_not_all]
ex_intro2 [constructor, in ex_intro2]
ex_inverse_impl_morphism [instance, in ex_inverse_impl_morphism]
ex_iff_morphism [instance, in ex_iff_morphism]
ex2 [inductive, in ex2]
E1 [definition, in E1]
E1_cvg [lemma, in E1_cvg]