Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (21446 entries) |

Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (889 entries) |

Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (714 entries) |

Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1464 entries) |

Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (482 entries) |

Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (10031 entries) |

Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (663 entries) |

Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (537 entries) |

Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (374 entries) |

Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (285 entries) |

Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (457 entries) |

Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (616 entries) |

Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1328 entries) |

Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3469 entries) |

Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (137 entries) |

## T

t [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]t [inductive, in Coq.Vectors.Fin]

t [definition, in Coq.Init.Nat]

t [inductive, in Coq.micromega.VarMap]

t [inductive, in Coq.Vectors.VectorDef]

Tactics [library]

Tactics [library]

tactic_view [constructor, in Coq.ssr.ssreflect]

Tadd [definition, in Coq.rtauto.Bintree]

tag [definition, in Coq.ssr.ssrfun]

Tag [section, in Coq.ssr.ssrfun]

Tagged [definition, in Coq.ssr.ssrfun]

tagged [definition, in Coq.ssr.ssrfun]

Tagged2 [definition, in Coq.ssr.ssrfun]

tagged2 [definition, in Coq.ssr.ssrfun]

tagged2' [definition, in Coq.ssr.ssrfun]

Tag.i [variable, in Coq.ssr.ssrfun]

Tag.I [variable, in Coq.ssr.ssrfun]

Tag.T_ [variable, in Coq.ssr.ssrfun]

Tag.U_ [variable, in Coq.ssr.ssrfun]

tag2 [definition, in Coq.ssr.ssrfun]

tail [definition, in Coq.micromega.Env]

tail [abbreviation, in Coq.Lists.List]

tail_mult [definition, in Coq.Arith.Mult]

tail_plus [definition, in Coq.Arith.Plus]

tail0 [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]

tail031 [definition, in Coq.Numbers.Cyclic.Int31.Int31]

tail031_equiv [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]

tail031_alt [definition, in Coq.Numbers.Cyclic.Int31.Cyclic31]

take [definition, in Coq.Vectors.VectorDef]

take_prf_irr [lemma, in Coq.Vectors.VectorSpec]

take_app [lemma, in Coq.Vectors.VectorSpec]

take_idem [lemma, in Coq.Vectors.VectorSpec]

take_O [lemma, in Coq.Vectors.VectorSpec]

tan [definition, in Coq.Reals.Rtrigo1]

tand [definition, in Coq.Reals.Rtrigo_calc]

tanh [definition, in Coq.Reals.Rtrigo_def]

tan_2PI3 [lemma, in Coq.Reals.Rtrigo_calc]

tan_PI3 [lemma, in Coq.Reals.Rtrigo_calc]

tan_PI6 [lemma, in Coq.Reals.Rtrigo_calc]

tan_PI4 [lemma, in Coq.Reals.Rtrigo_calc]

tan_2PI [lemma, in Coq.Reals.Rtrigo_calc]

tan_PI [lemma, in Coq.Reals.Rtrigo_calc]

tan_incr_1 [lemma, in Coq.Reals.Rtrigo1]

tan_incr_0 [lemma, in Coq.Reals.Rtrigo1]

tan_increasing_1 [lemma, in Coq.Reals.Rtrigo1]

tan_increasing_0 [lemma, in Coq.Reals.Rtrigo1]

tan_diff [lemma, in Coq.Reals.Rtrigo1]

tan_lt_0 [lemma, in Coq.Reals.Rtrigo1]

tan_gt_0 [lemma, in Coq.Reals.Rtrigo1]

tan_minus [lemma, in Coq.Reals.Rtrigo1]

tan_neg [lemma, in Coq.Reals.Rtrigo1]

tan_0 [lemma, in Coq.Reals.Rtrigo1]

tan_2a [lemma, in Coq.Reals.Rtrigo1]

tan_plus [lemma, in Coq.Reals.Rtrigo1]

tan_1_gt_1 [lemma, in Coq.Reals.Ratan]

tan_is_inj [lemma, in Coq.Reals.Ratan]

tan_increasing [lemma, in Coq.Reals.Ratan]

Tauto [library]

Tauto [library]

tauto_checker_sound [lemma, in Coq.micromega.Tauto]

tauto_checker [definition, in Coq.micromega.Tauto]

Tcons [constructor, in Coq.Classes.RelationClasses]

tech [lemma, in Coq.Reals.Machin]

tech_single_z_r_R1 [lemma, in Coq.Reals.RIneq]

tech_Rgt_minus [lemma, in Coq.Reals.RIneq]

tech_Rplus [lemma, in Coq.Reals.RIneq]

tech_up [lemma, in Coq.Reals.R_Ifp]

tech_limit_contr [lemma, in Coq.Reals.Rlimit]

tech_limit [lemma, in Coq.Reals.Rlimit]

tech_pow_Rplus [lemma, in Coq.Reals.Rfunctions]

tech_pow_Rmult [lemma, in Coq.Reals.Rfunctions]

tech_opp_tan [lemma, in Coq.Reals.Ratan]

tech1 [lemma, in Coq.Reals.PartSum]

tech11 [lemma, in Coq.Reals.PartSum]

tech12 [lemma, in Coq.Reals.PartSum]

tech13 [lemma, in Coq.Reals.SeqProp]

tech2 [lemma, in Coq.Reals.PartSum]

tech3 [lemma, in Coq.Reals.PartSum]

tech4 [lemma, in Coq.Reals.PartSum]

tech5 [lemma, in Coq.Reals.PartSum]

tech6 [lemma, in Coq.Reals.PartSum]

tech7 [lemma, in Coq.Reals.PartSum]

tech8 [lemma, in Coq.Reals.ArithProp]

tech9 [lemma, in Coq.Reals.SeqProp]

Tempty [constructor, in Coq.rtauto.Bintree]

ternary_operation [definition, in Coq.Classes.RelationClasses]

testbit [abbreviation, in Coq.Numbers.Natural.Peano.NPeano]

testbit [definition, in Coq.Init.Nat]

testbit_bitwise_2 [abbreviation, in Coq.Numbers.Natural.Peano.NPeano]

testbit_bitwise_1 [abbreviation, in Coq.Numbers.Natural.Peano.NPeano]

testbit_even_succ [abbreviation, in Coq.Numbers.Natural.Peano.NPeano]

testbit_odd_succ [abbreviation, in Coq.Numbers.Natural.Peano.NPeano]

testbit_even_0 [abbreviation, in Coq.Numbers.Natural.Peano.NPeano]

testbit_odd_0 [abbreviation, in Coq.Numbers.Natural.Peano.NPeano]

testbit_0_l [abbreviation, in Coq.Numbers.Natural.Peano.NPeano]

TestOrder [section, in Coq.Numbers.Integer.Binary.ZBinary]

TestOrder [section, in Coq.NArith.NArith]

TestOrder [section, in Coq.Arith.PeanoNat]

TestOrder.test [variable, in Coq.Numbers.Integer.Binary.ZBinary]

TestOrder.test [variable, in Coq.NArith.NArith]

TestOrder.test [variable, in Coq.Arith.PeanoNat]

TestRing [section, in Coq.Numbers.Cyclic.Int31.Ring31]

TestRing.test [variable, in Coq.Numbers.Cyclic.Int31.Ring31]

test_field [definition, in Coq.QArith.Qcanon]

Tget [definition, in Coq.rtauto.Bintree]

Tget_Tmap [lemma, in Coq.rtauto.Bintree]

Tget_Tadd [lemma, in Coq.rtauto.Bintree]

Tget_Tempty [lemma, in Coq.rtauto.Bintree]

tg_alt [definition, in Coq.Reals.AltSeries]

TheCanonical [module, in Coq.ssr.ssreflect]

TheCanonical.get [definition, in Coq.ssr.ssreflect]

TheCanonical.get_by [definition, in Coq.ssr.ssreflect]

TheCanonical.Put [constructor, in Coq.ssr.ssreflect]

TheCanonical.put [inductive, in Coq.ssr.ssreflect]

The_power_set_partial_order.U [variable, in Coq.Sets.Powerset]

The_power_set_partial_order [section, in Coq.Sets.Powerset]

this [projection, in Coq.QArith.Qcanon]

tl [definition, in Coq.Lists.Streams]

tl [definition, in Coq.Vectors.VectorDef]

tl [definition, in Coq.Lists.List]

Tlist [inductive, in Coq.Classes.RelationClasses]

tl_nth_tl [lemma, in Coq.Lists.Streams]

Tmap [definition, in Coq.rtauto.Bintree]

Tmap_Tadd [lemma, in Coq.rtauto.Bintree]

Tn [definition, in Coq.Numbers.Cyclic.Int31.Int31]

Tnil [constructor, in Coq.Classes.RelationClasses]

tn1_trans_equiv [abbreviation, in Coq.Relations.Operators_Properties]

tn1_trans [abbreviation, in Coq.Relations.Operators_Properties]

tn1_trans [constructor, in Coq.Relations.Relation_Operators]

tn1_step [constructor, in Coq.Relations.Relation_Operators]

toDeg [definition, in Coq.Reals.Rtrigo_calc]

TOMaxEqDec_to_OTF [module, in Coq.Structures.GenericMinMax]

TOMaxEqDec_to_Compare.compare_spec [lemma, in Coq.Structures.GenericMinMax]

TOMaxEqDec_to_Compare.compare [definition, in Coq.Structures.GenericMinMax]

TOMaxEqDec_to_Compare [module, in Coq.Structures.GenericMinMax]

topred [projection, in Coq.ssr.ssrbool]

topredE [lemma, in Coq.ssr.ssrbool]

toRad [definition, in Coq.Reals.Rtrigo_calc]

toRad_inj [lemma, in Coq.Reals.Rtrigo_calc]

total [definition, in Coq.ssr.ssrbool]

TotalLeBool [module, in Coq.Structures.Orders]

TotalLeBool' [module, in Coq.Structures.Orders]

Totally_ordered_definition [constructor, in Coq.Sets.Cpo]

Totally_ordered [inductive, in Coq.Sets.Cpo]

TotalOrder [module, in Coq.Structures.Orders]

TotalOrder' [module, in Coq.Structures.Orders]

TotalTransitiveLeBool [module, in Coq.Structures.Orders]

TotalTransitiveLeBool' [module, in Coq.Structures.Orders]

total_order_T [axiom, in Coq.Reals.Raxioms]

to_list_of_list_opp [lemma, in Coq.Vectors.VectorSpec]

to_nat [abbreviation, in Coq.micromega.RMicromega]

to_Z [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]

to_nat_inj [lemma, in Coq.Vectors.Fin]

to_nat_of_nat [lemma, in Coq.Vectors.Fin]

to_nat [definition, in Coq.Vectors.Fin]

to_list [definition, in Coq.Vectors.VectorDef]

Transitive [record, in Coq.Classes.CRelationClasses]

Transitive [inductive, in Coq.Classes.CRelationClasses]

transitive [definition, in Coq.ssr.ssrbool]

Transitive [definition, in Coq.Sets.Relations_1]

transitive [definition, in Coq.Relations.Relation_Definitions]

Transitive [record, in Coq.Classes.RelationClasses]

Transitive [inductive, in Coq.Classes.RelationClasses]

Transitive_Closure.R [variable, in Coq.Relations.Relation_Operators]

Transitive_Closure.A [variable, in Coq.Relations.Relation_Operators]

Transitive_Closure [section, in Coq.Relations.Relation_Operators]

Transitive_Closure [library]

transitivity [projection, in Coq.Classes.CRelationClasses]

transitivity [constructor, in Coq.Classes.CRelationClasses]

transitivity [projection, in Coq.Classes.RelationClasses]

transitivity [constructor, in Coq.Classes.RelationClasses]

Translation [section, in Coq.btauto.Reflect]

translation_0 [lemma, in Coq.Reals.Rgeom]

transp [definition, in Coq.Relations.Relation_Operators]

transpose [definition, in Coq.Lists.SetoidList]

transpose_restr2 [definition, in Coq.Lists.SetoidList]

transpose_restr [definition, in Coq.Lists.SetoidList]

transpose2 [definition, in Coq.Lists.SetoidList]

trans_co_eq_inv_impl_morphism [instance, in Coq.Classes.Morphisms]

trans_sym_contra_impl_morphism [instance, in Coq.Classes.Morphisms]

trans_sym_co_inv_impl_morphism [instance, in Coq.Classes.Morphisms]

trans_co_impl_morphism [instance, in Coq.Classes.Morphisms]

trans_contra_inv_impl_morphism [instance, in Coq.Classes.Morphisms]

trans_contra_co_morphism [instance, in Coq.Classes.Morphisms]

trans_EqSt [lemma, in Coq.Lists.Streams]

trans_JMeq [abbreviation, in Coq.Logic.JMeq]

trans_rtn1 [abbreviation, in Coq.Relations.Operators_Properties]

trans_rt1n [abbreviation, in Coq.Relations.Operators_Properties]

trans_t1n [abbreviation, in Coq.Relations.Operators_Properties]

trans_tn1 [abbreviation, in Coq.Relations.Operators_Properties]

trans_equal [abbreviation, in Coq.Init.Logic]

trans_eq [abbreviation, in Coq.Init.Logic]

trans_ord [definition, in Coq.Structures.OrdersTac]

trans_sym_eq [lemma, in Coq.Logic.Eqdep_dec]

trans_clos [abbreviation, in Coq.Wellfounded.Transitive_Closure]

trans_id [abbreviation, in Coq.Init.Logic_Type]

trans_eq_bool [lemma, in Coq.Bool.Bool]

trans_co_eq_inv_arrow_morphism [instance, in Coq.Classes.CMorphisms]

trans_sym_contra_arrow_morphism [instance, in Coq.Classes.CMorphisms]

trans_sym_co_inv_impl_type_morphism [instance, in Coq.Classes.CMorphisms]

trans_co_impl_type_morphism [instance, in Coq.Classes.CMorphisms]

trans_contra_inv_impl_type_morphism [instance, in Coq.Classes.CMorphisms]

trans_contra_co_type_morphism [instance, in Coq.Classes.CMorphisms]

Tree [inductive, in Coq.Sorting.Heap]

Tree [inductive, in Coq.rtauto.Bintree]

treesort [lemma, in Coq.Sorting.Heap]

treesort_twist2 [lemma, in Coq.Sets.Multiset]

treesort_twist1 [lemma, in Coq.Sets.Multiset]

treesort_twist2 [lemma, in Coq.Sets.Uniset]

treesort_twist1 [lemma, in Coq.Sets.Uniset]

Tree_Node [constructor, in Coq.Sorting.Heap]

Tree_Leaf [constructor, in Coq.Sorting.Heap]

Tremove [definition, in Coq.rtauto.Bintree]

triangle [lemma, in Coq.Reals.Rgeom]

triangle_rectangle_le [lemma, in Coq.Reals.R_sqr]

triangle_rectangle_lt [lemma, in Coq.Reals.R_sqr]

triangle_rectangle [lemma, in Coq.Reals.R_sqr]

Triple [inductive, in Coq.Sets.Ensembles]

Triple_r [constructor, in Coq.Sets.Ensembles]

Triple_m [constructor, in Coq.Sets.Ensembles]

Triple_l [constructor, in Coq.Sets.Ensembles]

Triple_as_Couple_Singleton [lemma, in Coq.Sets.Powerset_facts]

Triple_as_Couple [lemma, in Coq.Sets.Powerset_facts]

Triple_as_union [lemma, in Coq.Sets.Powerset_facts]

triv_nat [lemma, in Coq.Sets.Integers]

triv_div_th [lemma, in Coq.setoid_ring.InitialRing]

triv_div [definition, in Coq.setoid_ring.InitialRing]

True [inductive, in Coq.Init.Logic]

true [constructor, in Coq.Init.Datatypes]

trueP [constructor, in Coq.Logic.ClassicalFacts]

TrueP [definition, in Coq.Logic.ClassicalFacts]

true_predicate [definition, in Coq.Classes.RelationClasses]

true_xorb [abbreviation, in Coq.Bool.Bool]

trunc [lemma, in Coq.Vectors.VectorDef]

tt [constructor, in Coq.Init.Datatypes]

tt [definition, in Coq.micromega.Tauto]

TT [constructor, in Coq.micromega.Tauto]

TTLB_to_OTF.le_lteq [definition, in Coq.Structures.Orders]

TTLB_to_OTF.lt_compat [instance, in Coq.Structures.Orders]

TTLB_to_OTF.lt_strorder [instance, in Coq.Structures.Orders]

TTLB_to_OTF.eq_equiv [instance, in Coq.Structures.Orders]

TTLB_to_OTF.eqb_eq [lemma, in Coq.Structures.Orders]

TTLB_to_OTF.eqb [definition, in Coq.Structures.Orders]

TTLB_to_OTF.compare_spec [lemma, in Coq.Structures.Orders]

TTLB_to_OTF.compare [definition, in Coq.Structures.Orders]

TTLB_to_OTF.lt [definition, in Coq.Structures.Orders]

TTLB_to_OTF.eq [definition, in Coq.Structures.Orders]

TTLB_to_OTF.le [definition, in Coq.Structures.Orders]

TTLB_to_OTF.t [definition, in Coq.Structures.Orders]

TTLB_to_OTF [module, in Coq.Structures.Orders]

twice [definition, in Coq.Numbers.Cyclic.Int31.Int31]

twice_or_twice_plus_one [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]

twice_zero [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]

twice_plus_one [definition, in Coq.Numbers.Cyclic.Int31.Int31]

twist [lemma, in Coq.Sets.Permut]

two [definition, in Coq.Init.Nat]

Twon [definition, in Coq.Numbers.Cyclic.Int31.Int31]

two_p_pred [lemma, in Coq.ZArith.Zpower]

two_p_S [lemma, in Coq.ZArith.Zpower]

two_p_gt_ZERO [lemma, in Coq.ZArith.Zpower]

two_p_is_exp [lemma, in Coq.ZArith.Zpower]

two_p_correct [lemma, in Coq.ZArith.Zpower]

two_power_pos_is_exp [lemma, in Coq.ZArith.Zpower]

two_power_pos_correct [lemma, in Coq.ZArith.Zpower]

two_power_pos_nat [lemma, in Coq.ZArith.Zpower]

two_power_nat_correct [lemma, in Coq.ZArith.Zpower]

two_power_nat_S [lemma, in Coq.ZArith.Zpower]

two_p_equiv [lemma, in Coq.ZArith.Zpower]

two_power_pos_equiv [lemma, in Coq.ZArith.Zpower]

two_power_nat_equiv [lemma, in Coq.ZArith.Zpower]

two_p [definition, in Coq.ZArith.Zpower]

two_power_pos [definition, in Coq.ZArith.Zpower]

two_power_nat [definition, in Coq.ZArith.Zpower]

two_p_power2 [lemma, in Coq.Numbers.Cyclic.ZModulo.ZModulo]

two_or_two_plus_one [abbreviation, in Coq.ZArith.Zcomplements]

two_compl_to_Z_to_two_compl [lemma, in Coq.ZArith.Zdigits]

two_compl_value_Sn [lemma, in Coq.ZArith.Zdigits]

two_compl_value [lemma, in Coq.ZArith.Zdigits]

Typ [module, in Coq.Structures.Equalities]

TypElt [module, in Coq.MSets.MSetInterface]

TypElt.elt [axiom, in Coq.MSets.MSetInterface]

TypElt.t [axiom, in Coq.MSets.MSetInterface]

TypeNeqSmallType [module, in Coq.Logic.Hurkens]

TypeNeqSmallType.paradox [lemma, in Coq.Logic.Hurkens]

TypeNeqSmallType.Paradox [section, in Coq.Logic.Hurkens]

TypeNeqSmallType.Paradox.A [variable, in Coq.Logic.Hurkens]

TypeNeqSmallType.Paradox.down [variable, in Coq.Logic.Hurkens]

TypeNeqSmallType.Paradox.h [variable, in Coq.Logic.Hurkens]

TypeNeqSmallType.Paradox.U [variable, in Coq.Logic.Hurkens]

TypeNeqSmallType.Paradox.up [variable, in Coq.Logic.Hurkens]

TypeNeqSmallType.up_down [lemma, in Coq.Logic.Hurkens]

Type_with_equality.Filter [section, in Coq.Lists.SetoidList]

Type_with_equality.EqlistA [section, in Coq.Lists.SetoidList]

Type_with_equality.sotrans [variable, in Coq.Lists.SetoidList]

Type_with_equality.ltA_compat [variable, in Coq.Lists.SetoidList]

Type_with_equality.ltA_strorder [variable, in Coq.Lists.SetoidList]

Type_with_equality.ltA [variable, in Coq.Lists.SetoidList]

Type_with_equality.Remove.eqA_dec [variable, in Coq.Lists.SetoidList]

Type_with_equality.Remove [section, in Coq.Lists.SetoidList]

Type_with_equality.Fold2.Tra [variable, in Coq.Lists.SetoidList]

Type_with_equality.Fold2.Fold2_With_Restriction.TraR [variable, in Coq.Lists.SetoidList]

Type_with_equality.Fold2.Fold2_With_Restriction.R_compat [variable, in Coq.Lists.SetoidList]

Type_with_equality.Fold2.Fold2_With_Restriction.R_sym [variable, in Coq.Lists.SetoidList]

Type_with_equality.Fold2.Fold2_With_Restriction.R [variable, in Coq.Lists.SetoidList]

Type_with_equality.Fold2.Fold2_With_Restriction [section, in Coq.Lists.SetoidList]

Type_with_equality.Fold2.Comp [variable, in Coq.Lists.SetoidList]

Type_with_equality.Fold2.f [variable, in Coq.Lists.SetoidList]

Type_with_equality.Fold2.st [variable, in Coq.Lists.SetoidList]

Type_with_equality.Fold2.eqB [variable, in Coq.Lists.SetoidList]

Type_with_equality.Fold2.B [variable, in Coq.Lists.SetoidList]

Type_with_equality.Fold2 [section, in Coq.Lists.SetoidList]

Type_with_equality.Fold.Tra [variable, in Coq.Lists.SetoidList]

Type_with_equality.Fold.Fold_With_Restriction.TraR [variable, in Coq.Lists.SetoidList]

Type_with_equality.Fold.Fold_With_Restriction.R_compat [variable, in Coq.Lists.SetoidList]

Type_with_equality.Fold.Fold_With_Restriction.R_sym [variable, in Coq.Lists.SetoidList]

Type_with_equality.Fold.Fold_With_Restriction.R [variable, in Coq.Lists.SetoidList]

Type_with_equality.Fold.Fold_With_Restriction [section, in Coq.Lists.SetoidList]

Type_with_equality.Fold.Comp [variable, in Coq.Lists.SetoidList]

Type_with_equality.Fold.i [variable, in Coq.Lists.SetoidList]

Type_with_equality.Fold.f [variable, in Coq.Lists.SetoidList]

Type_with_equality.Fold.st [variable, in Coq.Lists.SetoidList]

Type_with_equality.Fold.eqB [variable, in Coq.Lists.SetoidList]

Type_with_equality.Fold.B [variable, in Coq.Lists.SetoidList]

Type_with_equality.Fold [section, in Coq.Lists.SetoidList]

Type_with_equality.EquivlistA [section, in Coq.Lists.SetoidList]

Type_with_equality.NoDupA [section, in Coq.Lists.SetoidList]

Type_with_equality.eqA_equiv [variable, in Coq.Lists.SetoidList]

Type_with_equality.eqA [variable, in Coq.Lists.SetoidList]

Type_with_equality.A [variable, in Coq.Lists.SetoidList]

Type_with_equality [section, in Coq.Lists.SetoidList]

Typ.t [axiom, in Coq.Structures.Equalities]

t_trans [constructor, in Coq.Relations.Relation_Operators]

t_step [constructor, in Coq.Relations.Relation_Operators]

t1n_trans_equiv [abbreviation, in Coq.Relations.Operators_Properties]

t1n_trans [abbreviation, in Coq.Relations.Operators_Properties]

t1n_trans [constructor, in Coq.Relations.Relation_Operators]

t1n_step [constructor, in Coq.Relations.Relation_Operators]

T31 [definition, in Coq.Numbers.Cyclic.Int31.Int31]

Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (21446 entries) |

Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (889 entries) |

Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (714 entries) |

Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1464 entries) |

Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (482 entries) |

Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (10031 entries) |

Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (663 entries) |

Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (537 entries) |

Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (374 entries) |

Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (285 entries) |

Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (457 entries) |

Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (616 entries) |

Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1328 entries) |

Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3469 entries) |

Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (137 entries) |