| 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 | (70451 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 | (1003 entries) |
| Binder 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 | (45703 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 | (771 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 | (1516 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 | (579 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 | (11670 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 | (1018 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 | (622 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 | (304 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 | (472 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 | (482 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 | (844 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 | (1187 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 | (4117 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 | (163 entries) |
T
t [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]t [definition, in Coq.Init.Nat]
t [inductive, in Coq.Vectors.Fin]
t [abbreviation, in Coq.micromega.VarMap]
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_of_sig [definition, in Coq.ssr.ssrfun]
tag_of_tag2 [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 [abbreviation, in Coq.Lists.List]
tail [definition, in Coq.micromega.Env]
tail_mul [definition, in Coq.Init.Nat]
tail_addmul [definition, in Coq.Init.Nat]
tail_add [definition, in Coq.Init.Nat]
tail_plus [definition, in Coq.Arith.Plus]
tail_mult [definition, in Coq.Arith.Mult]
tail0 [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
tail0 [axiom, in Coq.Numbers.Cyclic.Int63.Int63]
tail0_spec [axiom, in Coq.Numbers.Cyclic.Int63.Int63]
tail00_spec [lemma, in Coq.Numbers.Cyclic.Int63.Int63]
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_pi_plus [lemma, in Coq.Reals.Rtrigo_facts]
tan_pi_minus [lemma, in Coq.Reals.Rtrigo_facts]
tan_cos_opp [lemma, in Coq.Reals.Rtrigo_facts]
tan_cos [lemma, in Coq.Reals.Rtrigo_facts]
tan_sin_opp [lemma, in Coq.Reals.Rtrigo_facts]
tan_sin [lemma, in Coq.Reals.Rtrigo_facts]
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_acos [lemma, in Coq.Reals.Ratan]
tan_asin [lemma, in Coq.Reals.Ratan]
tan_atan [lemma, in Coq.Reals.Ratan]
tan_1_gt_1 [lemma, in Coq.Reals.Ratan]
tan_is_inj [abbreviation, in Coq.Reals.Ratan]
tan_inj [lemma, in Coq.Reals.Ratan]
tan_increasing [lemma, in Coq.Reals.Ratan]
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]
target [projection, in Coq.micromega.ZifyClasses]
target_prop [projection, in Coq.micromega.ZifyClasses]
Tauto [library]
Tauto [library]
tauto_checker_sound [lemma, in Coq.micromega.Tauto]
tauto_checker [definition, in Coq.micromega.Tauto]
TA':105 [binder, in Coq.micromega.Tauto]
TA:104 [binder, in Coq.micromega.Tauto]
TA:3 [binder, in Coq.micromega.Tauto]
TBOp [projection, in Coq.micromega.ZifyClasses]
TBOpInj [projection, in Coq.micromega.ZifyClasses]
TBOPINJ:119 [binder, in Coq.micromega.ZifyClasses]
TBOP:116 [binder, in Coq.micromega.ZifyClasses]
Tcons [constructor, in Coq.Classes.RelationClasses]
TCst [projection, in Coq.micromega.ZifyClasses]
TCstInj [projection, in Coq.micromega.ZifyClasses]
tearing_elem_fst [definition, in Coq.Reals.Runcountable]
tearing_sequences_ordered_forall [lemma, in Coq.Reals.Runcountable]
tearing_sequences_inc_dec [lemma, in Coq.Reals.Runcountable]
tearing_sequences_projsig [lemma, in Coq.Reals.Runcountable]
tearing_sequences [definition, in Coq.Reals.Runcountable]
tech [lemma, in Coq.Reals.Machin]
tech_up [lemma, in Coq.Reals.R_Ifp]
tech_pow_Rplus [lemma, in Coq.Reals.Rfunctions]
tech_pow_Rmult [lemma, in Coq.Reals.Rfunctions]
tech_limit_contr [lemma, in Coq.Reals.Rlimit]
tech_limit [lemma, in Coq.Reals.Rlimit]
tech_opp_tan [lemma, in Coq.Reals.Ratan]
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]
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]
ten [abbreviation, in Coq.Init.Nat]
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.Arith.PeanoNat]
TestOrder [section, in Coq.NArith.NArith]
TestOrder [section, in Coq.Numbers.Integer.Binary.ZBinary]
TestOrder.test [variable, in Coq.Arith.PeanoNat]
TestOrder.test [variable, in Coq.NArith.NArith]
TestOrder.test [variable, in Coq.Numbers.Integer.Binary.ZBinary]
TestRing [section, in Coq.Numbers.Cyclic.Int63.Ring63]
TestRing [section, in Coq.Numbers.Cyclic.Int31.Ring31]
TestRing.test [variable, in Coq.Numbers.Cyclic.Int63.Ring63]
TestRing.test [variable, in Coq.Numbers.Cyclic.Int31.Ring31]
test_field [definition, in Coq.QArith.Qcanon]
test:138 [binder, in Coq.ssr.ssreflect]
TFormula [definition, in Coq.micromega.Tauto]
tf2:350 [binder, in Coq.micromega.Tauto]
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]
tg:141 [binder, in Coq.micromega.ZMicromega]
tg:146 [binder, in Coq.micromega.ZMicromega]
tg:158 [binder, in Coq.micromega.ZMicromega]
tg:163 [binder, in Coq.micromega.ZMicromega]
tg:170 [binder, in Coq.micromega.ZMicromega]
tg:178 [binder, in Coq.micromega.ZMicromega]
tg:207 [binder, in Coq.micromega.Tauto]
tg:246 [binder, in Coq.micromega.RingMicromega]
tg:252 [binder, in Coq.micromega.RingMicromega]
tg:262 [binder, in Coq.micromega.RingMicromega]
tg:266 [binder, in Coq.micromega.RingMicromega]
tg:278 [binder, in Coq.micromega.RingMicromega]
tg:282 [binder, in Coq.micromega.RingMicromega]
tg:433 [binder, in Coq.micromega.Tauto]
tg:437 [binder, in Coq.micromega.Tauto]
tg:559 [binder, in Coq.micromega.Tauto]
tg:564 [binder, in Coq.micromega.Tauto]
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]
theta:41 [binder, in Coq.Reals.Rgeom]
theta:44 [binder, in Coq.Reals.Rgeom]
theta:53 [binder, in Coq.Reals.Rgeom]
theta:58 [binder, in Coq.Reals.Rgeom]
theta:65 [binder, in Coq.Reals.Rgeom]
theta:72 [binder, in Coq.Reals.Rgeom]
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.Lists.List]
tl [definition, in Coq.Vectors.VectorDef]
Tlist [inductive, in Coq.Classes.RelationClasses]
tl_nth_tl [lemma, in Coq.Lists.Streams]
tl':42 [binder, in Coq.Sorting.Permutation]
tl':51 [binder, in Coq.Sorting.Permutation]
tl:18 [binder, in Coq.Lists.List]
tl:357 [binder, in Coq.Lists.List]
tl:39 [binder, in Coq.Sorting.Permutation]
tl:41 [binder, in Coq.Sorting.Permutation]
tl:50 [binder, in Coq.Sorting.Permutation]
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]
toP:281 [binder, in Coq.ssr.ssrbool]
toRad [definition, in Coq.Reals.Rtrigo_calc]
toRad_inj [lemma, in Coq.Reals.Rtrigo_calc]
torn_number_below_second_sequence [lemma, in Coq.Reals.Runcountable]
torn_number_above_first_sequence [lemma, in Coq.Reals.Runcountable]
torn_number [definition, in Coq.Reals.Runcountable]
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 [lemma, in Coq.Reals.Rdefinitions]
to_list_of_list_opp [lemma, in Coq.Vectors.VectorSpec]
to_Z [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
to_bits_of_bits [lemma, in Coq.Init.Byte]
to_bits [definition, in Coq.Init.Byte]
to_list_inj [lemma, in Coq.Numbers.DecimalFacts]
to_list_of_list [lemma, in Coq.Numbers.DecimalFacts]
to_list [definition, in Coq.Numbers.DecimalFacts]
to_pos_of_pos [lemma, in Coq.Strings.OctalString]
to_nat_of_nat [lemma, in Coq.Strings.OctalString]
to_Z_of_Z [lemma, in Coq.Strings.OctalString]
to_N_of_N [lemma, in Coq.Strings.OctalString]
to_nat [definition, in Coq.Strings.OctalString]
to_Z [definition, in Coq.Strings.OctalString]
to_pos [definition, in Coq.Strings.OctalString]
to_N [definition, in Coq.Strings.OctalString]
to_pos_of_pos [lemma, in Coq.Strings.HexString]
to_nat_of_nat [lemma, in Coq.Strings.HexString]
to_Z_of_Z [lemma, in Coq.Strings.HexString]
to_N_of_N [lemma, in Coq.Strings.HexString]
to_nat [definition, in Coq.Strings.HexString]
to_Z [definition, in Coq.Strings.HexString]
to_pos [definition, in Coq.Strings.HexString]
to_N [definition, in Coq.Strings.HexString]
to_decimal_surj [lemma, in Coq.Numbers.DecimalQ]
to_decimal_inj [lemma, in Coq.Numbers.DecimalQ]
to_of [lemma, in Coq.Numbers.DecimalQ]
to_Z_split [lemma, in Coq.Numbers.Cyclic.Int63.Int63]
to_Z_gcd [lemma, in Coq.Numbers.Cyclic.Int63.Int63]
to_Z_inj [lemma, in Coq.Numbers.Cyclic.Int63.Int63]
to_Z_1 [lemma, in Coq.Numbers.Cyclic.Int63.Int63]
to_Z_0 [lemma, in Coq.Numbers.Cyclic.Int63.Int63]
to_Z_bounded [lemma, in Coq.Numbers.Cyclic.Int63.Int63]
to_Z_rec_bounded [lemma, in Coq.Numbers.Cyclic.Int63.Int63]
to_Z [definition, in Coq.Numbers.Cyclic.Int63.Int63]
to_Z_rec [definition, in Coq.Numbers.Cyclic.Int63.Int63]
to_num_int [definition, in Coq.Init.Nat]
to_hex_int [definition, in Coq.Init.Nat]
to_int [definition, in Coq.Init.Nat]
to_num_hex_uint [definition, in Coq.Init.Nat]
to_num_uint [definition, in Coq.Init.Nat]
to_hex_uint [definition, in Coq.Init.Nat]
to_little_hex_uint [definition, in Coq.Init.Nat]
to_uint [definition, in Coq.Init.Nat]
to_little_uint [definition, in Coq.Init.Nat]
to_Z_bounded [lemma, in Coq.micromega.ZifyInt63]
to_hex_number [definition, in Coq.Reals.Rdefinitions]
to_number [definition, in Coq.Reals.Rdefinitions]
to_hexadecimal [definition, in Coq.Reals.Rdefinitions]
to_decimal [definition, in Coq.Reals.Rdefinitions]
to_int_surj [lemma, in Coq.Numbers.DecimalZ]
to_int_inj [lemma, in Coq.Numbers.DecimalZ]
to_of [lemma, in Coq.Numbers.DecimalZ]
to_list_inj [lemma, in Coq.Numbers.HexadecimalFacts]
to_list_of_list [lemma, in Coq.Numbers.HexadecimalFacts]
to_list [definition, in Coq.Numbers.HexadecimalFacts]
to_pos_of_pos [lemma, in Coq.Strings.BinaryString]
to_nat_of_nat [lemma, in Coq.Strings.BinaryString]
to_N_of_N [lemma, in Coq.Strings.BinaryString]
to_nat [definition, in Coq.Strings.BinaryString]
to_Z [definition, in Coq.Strings.BinaryString]
to_pos [definition, in Coq.Strings.BinaryString]
to_N [definition, in Coq.Strings.BinaryString]
to_int_surj [lemma, in Coq.Numbers.HexadecimalZ]
to_int_inj [lemma, in Coq.Numbers.HexadecimalZ]
to_of [lemma, in Coq.Numbers.HexadecimalZ]
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_hexadecimal_surj [lemma, in Coq.Numbers.HexadecimalR]
to_hexadecimal_inj [lemma, in Coq.Numbers.HexadecimalR]
to_of [lemma, in Coq.Numbers.HexadecimalR]
to_nat_via_N [lemma, in Coq.Strings.Byte]
to_N_via_nat [lemma, in Coq.Strings.Byte]
to_N_bounded [lemma, in Coq.Strings.Byte]
to_of_N_option_map [lemma, in Coq.Strings.Byte]
to_of_N_iff [lemma, in Coq.Strings.Byte]
to_of_N [lemma, in Coq.Strings.Byte]
to_N [definition, in Coq.Strings.Byte]
to_nat_bounded [lemma, in Coq.Strings.Byte]
to_of_nat_option_map [lemma, in Coq.Strings.Byte]
to_of_nat_iff [lemma, in Coq.Strings.Byte]
to_of_nat [lemma, in Coq.Strings.Byte]
to_nat [definition, in Coq.Strings.Byte]
to_hexadecimal_surj [lemma, in Coq.Numbers.HexadecimalQ]
to_hexadecimal_inj [lemma, in Coq.Numbers.HexadecimalQ]
to_of [lemma, in Coq.Numbers.HexadecimalQ]
to_decimal_surj [lemma, in Coq.Numbers.DecimalR]
to_decimal_inj [lemma, in Coq.Numbers.DecimalR]
to_of [lemma, in Coq.Numbers.DecimalR]
to_nat [abbreviation, in Coq.micromega.RMicromega]
to_constr:291 [binder, in Coq.micromega.Tauto]
to_constrT [record, in Coq.micromega.Tauto]
to_list [definition, in Coq.Vectors.VectorDef]
to_Bvector [definition, in Coq.Strings.ByteVector]
to_string [definition, in Coq.Strings.ByteVector]
to_hex_number [definition, in Coq.QArith.QArith_base]
to_number [definition, in Coq.QArith.QArith_base]
to_hexadecimal [definition, in Coq.QArith.QArith_base]
to_decimal [definition, in Coq.QArith.QArith_base]
TR [projection, in Coq.micromega.ZifyClasses]
transb:44 [binder, in Coq.Classes.CEquivalence]
transb:44 [binder, in Coq.Classes.Equivalence]
Transitive [record, in Coq.Classes.RelationClasses]
Transitive [inductive, in Coq.Classes.RelationClasses]
transitive [definition, in Coq.ssr.ssrbool]
Transitive [record, in Coq.Classes.CRelationClasses]
Transitive [inductive, in Coq.Classes.CRelationClasses]
Transitive [definition, in Coq.Sets.Relations_1]
transitive [definition, in Coq.Relations.Relation_Definitions]
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.RelationClasses]
transitivity [constructor, in Coq.Classes.RelationClasses]
transitivity [projection, in Coq.Classes.CRelationClasses]
transitivity [constructor, in Coq.Classes.CRelationClasses]
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_EqSt [lemma, in Coq.Lists.Streams]
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_sym_eq [lemma, in Coq.Logic.Eqdep_dec]
trans_clos [abbreviation, in Coq.Wellfounded.Transitive_Closure]
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_JMeq [abbreviation, in Coq.Logic.JMeq]
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]
trans_equal [abbreviation, in Coq.Init.Logic]
trans_eq [abbreviation, in Coq.Init.Logic]
trans_ord [definition, in Coq.Structures.OrdersTac]
Tree [abbreviation, in Coq.rtauto.Bintree]
Tree [inductive, in Coq.rtauto.Bintree]
Tree [inductive, in Coq.Sorting.Heap]
treesort [lemma, in Coq.Sorting.Heap]
treesort_twist2 [lemma, in Coq.Sets.Uniset]
treesort_twist1 [lemma, in Coq.Sets.Uniset]
treesort_twist2 [lemma, in Coq.Sets.Multiset]
treesort_twist1 [lemma, in Coq.Sets.Multiset]
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]
TRInj [projection, in Coq.micromega.ZifyClasses]
TRINJ:146 [binder, in Coq.micromega.ZifyClasses]
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_div_th [lemma, in Coq.setoid_ring.InitialRing]
triv_div [definition, in Coq.setoid_ring.InitialRing]
triv_nat [lemma, in Coq.Sets.Integers]
true [constructor, in Coq.Init.Datatypes]
True [inductive, in Coq.Init.Logic]
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]
true_hprop [lemma, in Coq.Logic.HLevels]
trunc [lemma, in Coq.Vectors.VectorDef]
TR:143 [binder, in Coq.micromega.ZifyClasses]
tt [constructor, in Coq.Init.Datatypes]
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]
tt:511 [binder, in Coq.micromega.Tauto]
TUOp [projection, in Coq.micromega.ZifyClasses]
TUOpInj [projection, in Coq.micromega.ZifyClasses]
TUOPINJ:135 [binder, in Coq.micromega.ZifyClasses]
TUOP:133 [binder, in Coq.micromega.ZifyClasses]
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.Floats.PrimFloat]
two [definition, in Coq.Init.Nat]
Twon [definition, in Coq.Numbers.Cyclic.Int31.Int31]
twoPQ:121 [binder, in Coq.micromega.EnvRing]
two_p_power2 [lemma, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
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]
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_or_two_plus_one [abbreviation, in Coq.ZArith.Zcomplements]
TX:106 [binder, in Coq.micromega.Tauto]
TX:148 [binder, in Coq.micromega.Tauto]
TX:158 [binder, in Coq.micromega.Tauto]
TX:180 [binder, in Coq.micromega.ZMicromega]
TX:180 [binder, in Coq.micromega.Tauto]
TX:185 [binder, in Coq.micromega.Tauto]
TX:190 [binder, in Coq.micromega.Tauto]
TX:234 [binder, in Coq.micromega.Tauto]
TX:264 [binder, in Coq.micromega.Tauto]
tx:28 [binder, in Coq.Reals.Rgeom]
tx:37 [binder, in Coq.Reals.Rgeom]
TX:4 [binder, in Coq.micromega.Tauto]
TX:453 [binder, in Coq.micromega.Tauto]
TX:463 [binder, in Coq.micromega.Tauto]
TX:473 [binder, in Coq.micromega.Tauto]
TX:483 [binder, in Coq.micromega.Tauto]
TX:493 [binder, in Coq.micromega.Tauto]
tx:63 [binder, in Coq.Reals.Rgeom]
tx:70 [binder, in Coq.Reals.Rgeom]
TX:75 [binder, in Coq.micromega.QMicromega]
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]
ty:30 [binder, in Coq.Reals.Rgeom]
ty:38 [binder, in Coq.Reals.Rgeom]
ty:64 [binder, in Coq.Reals.Rgeom]
ty:71 [binder, in Coq.Reals.Rgeom]
T_:121 [binder, in Coq.ssr.ssrfun]
t_encad:78 [binder, in Coq.Reals.Ratan]
t_trans [constructor, in Coq.Relations.Relation_Operators]
t_step [constructor, in Coq.Relations.Relation_Operators]
t':221 [binder, in Coq.micromega.Tauto]
t':245 [binder, in Coq.micromega.Tauto]
t':251 [binder, in Coq.micromega.Tauto]
t':257 [binder, in Coq.micromega.Tauto]
t':263 [binder, in Coq.micromega.Tauto]
t':506 [binder, in Coq.micromega.Tauto]
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]
T1:10 [binder, in Coq.micromega.DeclConstant]
T1:109 [binder, in Coq.micromega.ZifyClasses]
T1:11 [binder, in Coq.micromega.ZifyClasses]
t1:11 [binder, in Coq.setoid_ring.Ncring_tac]
t1:110 [binder, in Coq.setoid_ring.Ncring_tac]
t1:1204 [binder, in Coq.FSets.FMapAVL]
t1:121 [binder, in Coq.micromega.ZifyClasses]
T1:128 [binder, in Coq.micromega.ZifyClasses]
t1:137 [binder, in Coq.micromega.ZifyClasses]
T1:14 [binder, in Coq.micromega.DeclConstant]
t1:148 [binder, in Coq.micromega.ZifyClasses]
t1:148 [binder, in Coq.setoid_ring.Ncring_tac]
t1:151 [binder, in Coq.MSets.MSetRBT]
t1:153 [binder, in Coq.MSets.MSetRBT]
t1:155 [binder, in Coq.micromega.ZifyClasses]
t1:156 [binder, in Coq.MSets.MSetRBT]
t1:159 [binder, in Coq.micromega.ZifyClasses]
t1:163 [binder, in Coq.micromega.ZifyClasses]
t1:163 [binder, in Coq.setoid_ring.Ncring_tac]
t1:167 [binder, in Coq.micromega.ZifyClasses]
t1:170 [binder, in Coq.micromega.ZifyClasses]
t1:185 [binder, in Coq.setoid_ring.Ncring_tac]
t1:238 [binder, in Coq.setoid_ring.Ncring_tac]
T1:25 [binder, in Coq.micromega.ZifyClasses]
T1:35 [binder, in Coq.Sorting.Heap]
T1:38 [binder, in Coq.Sorting.Heap]
T1:42 [binder, in Coq.Sorting.Heap]
T1:47 [binder, in Coq.Sorting.Heap]
t1:52 [binder, in Coq.Array.PArray]
T1:54 [binder, in Coq.rtauto.Bintree]
T1:62 [binder, in Coq.micromega.ZifyClasses]
t1:64 [binder, in Coq.Sorting.Heap]
T1:680 [binder, in Coq.ssr.ssrbool]
T1:70 [binder, in Coq.Sorting.Heap]
T1:71 [binder, in Coq.micromega.ZifyClasses]
t1:95 [binder, in Coq.setoid_ring.Ncring_tac]
T1:99 [binder, in Coq.ssr.ssrfun]
t2:10 [binder, in Coq.setoid_ring.Ncring_tac]
T2:100 [binder, in Coq.ssr.ssrfun]
T2:11 [binder, in Coq.micromega.DeclConstant]
T2:110 [binder, in Coq.micromega.ZifyClasses]
t2:112 [binder, in Coq.setoid_ring.Ncring_tac]
T2:12 [binder, in Coq.micromega.ZifyClasses]
t2:1205 [binder, in Coq.FSets.FMapAVL]
t2:124 [binder, in Coq.micromega.ZifyClasses]
T2:129 [binder, in Coq.micromega.ZifyClasses]
t2:135 [binder, in Coq.setoid_ring.Ncring_tac]
T2:15 [binder, in Coq.micromega.DeclConstant]
t2:150 [binder, in Coq.setoid_ring.Ncring_tac]
t2:151 [binder, in Coq.micromega.ZifyClasses]
t2:152 [binder, in Coq.MSets.MSetRBT]
t2:154 [binder, in Coq.MSets.MSetRBT]
t2:156 [binder, in Coq.micromega.ZifyClasses]
t2:157 [binder, in Coq.MSets.MSetRBT]
t2:160 [binder, in Coq.micromega.ZifyClasses]
t2:164 [binder, in Coq.micromega.ZifyClasses]
t2:168 [binder, in Coq.micromega.ZifyClasses]
T2:26 [binder, in Coq.micromega.ZifyClasses]
T2:36 [binder, in Coq.Sorting.Heap]
T2:39 [binder, in Coq.Sorting.Heap]
T2:43 [binder, in Coq.Sorting.Heap]
T2:48 [binder, in Coq.Sorting.Heap]
t2:53 [binder, in Coq.Array.PArray]
T2:55 [binder, in Coq.rtauto.Bintree]
T2:63 [binder, in Coq.micromega.ZifyClasses]
t2:65 [binder, in Coq.Sorting.Heap]
t2:69 [binder, in Coq.Vectors.VectorDef]
T2:72 [binder, in Coq.micromega.ZifyClasses]
t2:97 [binder, in Coq.setoid_ring.Ncring_tac]
T31 [definition, in Coq.Numbers.Cyclic.Int31.Int31]
T3:111 [binder, in Coq.micromega.ZifyClasses]
T3:13 [binder, in Coq.micromega.ZifyClasses]
T3:16 [binder, in Coq.micromega.DeclConstant]
T3:64 [binder, in Coq.micromega.ZifyClasses]
T3:689 [binder, in Coq.ssr.ssrbool]
T:1 [binder, in Coq.micromega.DeclConstant]
t:1 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
T:1 [binder, in Coq.setoid_ring.Ncring]
t:10 [binder, in Coq.MSets.MSetGenTree]
T:10 [binder, in Coq.setoid_ring.Ncring]
T:103 [binder, in Coq.ssr.ssrfun]
T:106 [binder, in Coq.rtauto.Bintree]
T:109 [binder, in Coq.rtauto.Bintree]
t:11 [binder, in Coq.MSets.MSetRBT]
t:11 [binder, in Coq.Sets.Relations_3_facts]
T:113 [binder, in Coq.rtauto.Bintree]
t:117 [binder, in Coq.Vectors.VectorDef]
T:119 [binder, in Coq.ssr.ssreflect]
t:12 [binder, in Coq.Array.PArray]
t:12 [binder, in Coq.Sets.Relations_3_facts]
t:120 [binder, in Coq.Reals.MVT]
t:120 [binder, in Coq.Vectors.VectorDef]
t:121 [binder, in Coq.MSets.MSetPositive]
t:123 [binder, in Coq.Reals.MVT]
t:124 [binder, in Coq.FSets.FSetPositive]
t:125 [binder, in Coq.QArith.Qcanon]
T:126 [binder, in Coq.ssr.ssrfun]
T:127 [binder, in Coq.ssr.ssreflect]
t:127 [binder, in Coq.micromega.Tauto]
T:128 [binder, in Coq.ssr.ssreflect]
t:13 [binder, in Coq.MSets.MSetRBT]
t:13 [binder, in Coq.MSets.MSetGenTree]
t:130 [binder, in Coq.Reals.MVT]
t:131 [binder, in Coq.Vectors.VectorDef]
T:132 [binder, in Coq.Classes.RelationClasses]
T:134 [binder, in Coq.ssr.ssrbool]
t:135 [binder, in Coq.micromega.Tauto]
T:136 [binder, in Coq.ssr.ssrfun]
t:137 [binder, in Coq.Reals.MVT]
t:139 [binder, in Coq.micromega.Tauto]
T:14 [binder, in Coq.setoid_ring.Ncring_tac]
T:140 [binder, in Coq.micromega.ZifyClasses]
T:140 [binder, in Coq.micromega.ZMicromega]
t:143 [binder, in Coq.MSets.MSetRBT]
t:145 [binder, in Coq.MSets.MSetRBT]
T:145 [binder, in Coq.micromega.ZMicromega]
T:156 [binder, in Coq.micromega.ZMicromega]
t:157 [binder, in Coq.micromega.ZMicromega]
t:159 [binder, in Coq.Numbers.DecimalFacts]
t:159 [binder, in Coq.Numbers.HexadecimalFacts]
t:16 [binder, in Coq.Reals.Cauchy.QExtra]
T:160 [binder, in Coq.micromega.ZMicromega]
t:162 [binder, in Coq.micromega.ZMicromega]
T:164 [binder, in Coq.ssr.ssrfun]
t:165 [binder, in Coq.Reals.Abstract.ConstructiveSum]
t:168 [binder, in Coq.MSets.MSetGenTree]
T:168 [binder, in Coq.micromega.ZMicromega]
t:169 [binder, in Coq.micromega.ZMicromega]
T:17 [binder, in Coq.setoid_ring.Ncring_tac]
t:17 [binder, in Coq.Array.PArray]
T:17 [binder, in Coq.ssr.ssrfun]
t:17 [binder, in Coq.Program.Equality]
t:171 [binder, in Coq.MSets.MSetRBT]
t:171 [binder, in Coq.MSets.MSetGenTree]
T:172 [binder, in Coq.ssr.ssrfun]
t:172 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
t:173 [binder, in Coq.MSets.MSetRBT]
t:173 [binder, in Coq.MSets.MSetGenTree]
t:173 [binder, in Coq.Reals.Abstract.ConstructiveSum]
t:175 [binder, in Coq.MSets.MSetRBT]
T:175 [binder, in Coq.micromega.ZMicromega]
t:176 [binder, in Coq.MSets.MSetGenTree]
t:177 [binder, in Coq.micromega.ZMicromega]
T:18 [binder, in Coq.setoid_ring.Ncring_tac]
t:18 [binder, in Coq.MSets.MSetGenTree]
t:180 [binder, in Coq.MSets.MSetRBT]
t:19 [binder, in Coq.setoid_ring.Ncring_tac]
T:19 [binder, in Coq.setoid_ring.Ncring]
t:190 [binder, in Coq.MSets.MSetRBT]
t:194 [binder, in Coq.Reals.RiemannInt]
t:194 [binder, in Coq.MSets.MSetRBT]
T:195 [binder, in Coq.micromega.RingMicromega]
t:195 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
t:196 [binder, in Coq.Reals.RiemannInt]
t:197 [binder, in Coq.setoid_ring.Ncring_tac]
t:197 [binder, in Coq.micromega.Tauto]
t:198 [binder, in Coq.MSets.MSetRBT]
T:2 [binder, in Coq.micromega.ZifyClasses]
t:2 [binder, in Coq.setoid_ring.Ncring_tac]
t:205 [binder, in Coq.micromega.Tauto]
t:21 [binder, in Coq.Reals.RiemannInt]
t:21 [binder, in Coq.Program.Equality]
t:211 [binder, in Coq.micromega.Tauto]
t:215 [binder, in Coq.Reals.RiemannInt]
t:215 [binder, in Coq.MSets.MSetRBT]
t:218 [binder, in Coq.Reals.RiemannInt]
t:219 [binder, in Coq.MSets.MSetRBT]
t:219 [binder, in Coq.micromega.Tauto]
t:221 [binder, in Coq.Reals.RiemannInt]
t:223 [binder, in Coq.MSets.MSetRBT]
t:224 [binder, in Coq.Reals.RiemannInt]
t:228 [binder, in Coq.MSets.MSetRBT]
t:23 [binder, in Coq.Array.PArray]
t:240 [binder, in Coq.micromega.RingMicromega]
T:244 [binder, in Coq.micromega.RingMicromega]
t:245 [binder, in Coq.QArith.QArith_base]
T:249 [binder, in Coq.micromega.RingMicromega]
t:249 [binder, in Coq.QArith.QArith_base]
t:25 [binder, in Coq.Program.Equality]
t:25 [binder, in Coq.Sorting.Heap]
t:250 [binder, in Coq.Reals.RiemannInt]
t:252 [binder, in Coq.Reals.RiemannInt]
T:255 [binder, in Coq.ssr.ssrbool]
T:256 [binder, in Coq.ssr.ssrbool]
T:260 [binder, in Coq.micromega.RingMicromega]
t:261 [binder, in Coq.micromega.RingMicromega]
t:263 [binder, in Coq.micromega.ZMicromega]
T:264 [binder, in Coq.micromega.RingMicromega]
t:265 [binder, in Coq.micromega.RingMicromega]
t:265 [binder, in Coq.Init.Logic]
t:266 [binder, in Coq.Reals.RiemannInt]
t:269 [binder, in Coq.Reals.RiemannInt]
T:27 [binder, in Coq.ssr.ssrfun]
T:274 [binder, in Coq.ssr.ssrbool]
T:274 [binder, in Coq.ssr.ssrfun]
T:275 [binder, in Coq.micromega.RingMicromega]
T:275 [binder, in Coq.ssr.ssrfun]
t:276 [binder, in Coq.Reals.RiemannInt]
T:276 [binder, in Coq.ssr.ssrfun]
t:277 [binder, in Coq.micromega.RingMicromega]
t:277 [binder, in Coq.micromega.ZMicromega]
T:278 [binder, in Coq.ssr.ssrbool]
T:279 [binder, in Coq.micromega.RingMicromega]
t:279 [binder, in Coq.Reals.RiemannInt]
T:279 [binder, in Coq.ssr.ssrfun]
T:28 [binder, in Coq.setoid_ring.Ncring]
t:281 [binder, in Coq.micromega.RingMicromega]
T:283 [binder, in Coq.ssr.ssrbool]
t:284 [binder, in Coq.Reals.RiemannInt]
T:284 [binder, in Coq.ssr.ssrbool]
T:285 [binder, in Coq.ssr.ssrbool]
T:286 [binder, in Coq.ssr.ssrbool]
t:287 [binder, in Coq.Reals.RiemannInt]
T:288 [binder, in Coq.ssr.ssrbool]
T:289 [binder, in Coq.ssr.ssrbool]
t:29 [binder, in Coq.Sets.Permut]
T:290 [binder, in Coq.ssr.ssrbool]
t:292 [binder, in Coq.Reals.RiemannInt]
T:293 [binder, in Coq.ssr.ssrbool]
t:295 [binder, in Coq.Reals.RiemannInt]
T:296 [binder, in Coq.ssr.ssrbool]
T:298 [binder, in Coq.ssr.ssrbool]
t:3 [binder, in Coq.Numbers.Cyclic.Int31.Int31]
T:30 [binder, in Coq.ssr.ssrfun]
t:30 [binder, in Coq.Reals.Cauchy.QExtra]
T:309 [binder, in Coq.ssr.ssrbool]
T:311 [binder, in Coq.ssr.ssrbool]
t:312 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
T:312 [binder, in Coq.ssr.ssrbool]
t:313 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
t:314 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
T:314 [binder, in Coq.ssr.ssrbool]
t:315 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
T:315 [binder, in Coq.ssr.ssrbool]
t:316 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
T:316 [binder, in Coq.ssr.ssrbool]
t:318 [binder, in Coq.Reals.RiemannInt]
t:32 [binder, in Coq.Reals.RiemannInt]
T:32 [binder, in Coq.ssr.ssreflect]
T:321 [binder, in Coq.ssr.ssrbool]
T:322 [binder, in Coq.ssr.ssrbool]
t:323 [binder, in Coq.Reals.RiemannInt]
t:326 [binder, in Coq.micromega.ZMicromega]
t:33 [binder, in Coq.setoid_ring.Ncring_tac]
t:33 [binder, in Coq.Array.PArray]
T:33 [binder, in Coq.ssr.ssrfun]
t:33 [binder, in Coq.Vectors.VectorDef]
T:333 [binder, in Coq.ssr.ssrbool]
T:336 [binder, in Coq.ssr.ssrbool]
t:34 [binder, in Coq.omega.OmegaLemmas]
t:34 [binder, in Coq.Reals.Cauchy.QExtra]
T:347 [binder, in Coq.ssr.ssrbool]
t:349 [binder, in Coq.MSets.MSetRBT]
T:35 [binder, in Coq.micromega.ZifyClasses]
T:35 [binder, in Coq.ssr.ssreflect]
T:350 [binder, in Coq.ssr.ssrbool]
T:353 [binder, in Coq.ssr.ssrbool]
t:355 [binder, in Coq.Reals.RiemannInt]
T:356 [binder, in Coq.ssr.ssrbool]
t:358 [binder, in Coq.Reals.RiemannInt]
T:359 [binder, in Coq.ssr.ssrbool]
t:359 [binder, in Coq.MSets.MSetRBT]
T:360 [binder, in Coq.ssr.ssrbool]
t:363 [binder, in Coq.Reals.RiemannInt]
T:363 [binder, in Coq.ssr.ssrbool]
t:366 [binder, in Coq.Reals.RiemannInt]
T:367 [binder, in Coq.ssr.ssrbool]
t:367 [binder, in Coq.micromega.Tauto]
t:369 [binder, in Coq.Reals.RiemannInt]
T:37 [binder, in Coq.setoid_ring.Ncring]
t:370 [binder, in Coq.micromega.ZMicromega]
T:371 [binder, in Coq.ssr.ssrbool]
t:372 [binder, in Coq.Reals.RiemannInt]
T:374 [binder, in Coq.ssr.ssrbool]
T:376 [binder, in Coq.ssr.ssrbool]
t:38 [binder, in Coq.Reals.Cauchy.QExtra]
t:384 [binder, in Coq.micromega.Tauto]
t:388 [binder, in Coq.Reals.RiemannInt]
t:389 [binder, in Coq.micromega.Tauto]
t:391 [binder, in Coq.ssr.ssrfun]
t:393 [binder, in Coq.Reals.RiemannInt]
T:399 [binder, in Coq.ssr.ssrbool]
T:4 [binder, in Coq.Logic.SetoidChoice]
T:4 [binder, in Coq.micromega.DeclConstant]
t:4 [binder, in Coq.MSets.MSetGenTree]
t:40 [binder, in Coq.Array.PArray]
T:40 [binder, in Coq.ssr.ssreflect]
t:40 [binder, in Coq.omega.OmegaLemmas]
T:400 [binder, in Coq.ssr.ssrbool]
T:401 [binder, in Coq.ssr.ssrbool]
t:402 [binder, in Coq.MSets.MSetRBT]
T:403 [binder, in Coq.ssr.ssrbool]
t:408 [binder, in Coq.Reals.RiemannInt]
t:409 [binder, in Coq.Reals.Rtopology]
T:41 [binder, in Coq.rtauto.Bintree]
t:410 [binder, in Coq.Reals.Rtopology]
t:411 [binder, in Coq.Reals.RiemannInt]
T:42 [binder, in Coq.micromega.ZifyClasses]
t:42 [binder, in Coq.Reals.RiemannInt]
t:44 [binder, in Coq.micromega.Refl]
t:44 [binder, in Coq.Vectors.VectorDef]
T:44 [binder, in Coq.Sorting.Heap]
T:448 [binder, in Coq.ssr.ssrbool]
t:45 [binder, in Coq.Array.PArray]
t:45 [binder, in Coq.Sets.Permut]
T:452 [binder, in Coq.ssr.ssrbool]
T:457 [binder, in Coq.ssr.ssrbool]
t:46 [binder, in Coq.Sets.Multiset]
T:46 [binder, in Coq.setoid_ring.Ncring]
t:47 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
t:473 [binder, in Coq.Reals.RiemannInt]
t:476 [binder, in Coq.Reals.RiemannInt]
t:48 [binder, in Coq.Reals.RiemannInt]
T:48 [binder, in Coq.rtauto.Bintree]
t:481 [binder, in Coq.Reals.RiemannInt]
t:484 [binder, in Coq.Reals.RiemannInt]
T:485 [binder, in Coq.ssr.ssrbool]
T:487 [binder, in Coq.ssr.ssrbool]
t:489 [binder, in Coq.Reals.RiemannInt]
t:49 [binder, in Coq.Array.PArray]
t:49 [binder, in Coq.Sets.Permut]
t:49 [binder, in Coq.micromega.Refl]
T:49 [binder, in Coq.Sorting.Heap]
T:491 [binder, in Coq.ssr.ssrbool]
t:492 [binder, in Coq.Reals.RiemannInt]
T:5 [binder, in Coq.ssr.ssrfun]
T:50 [binder, in Coq.Sorting.Heap]
t:502 [binder, in Coq.micromega.Tauto]
T:505 [binder, in Coq.ssr.ssrbool]
t:505 [binder, in Coq.micromega.Tauto]
T:513 [binder, in Coq.ssr.ssrbool]
t:52 [binder, in Coq.Reals.RiemannInt]
T:523 [binder, in Coq.ssr.ssrbool]
t:528 [binder, in Coq.micromega.Tauto]
t:53 [binder, in Coq.Sets.Multiset]
t:536 [binder, in Coq.micromega.Tauto]
T:55 [binder, in Coq.ssr.ssrbool]
T:55 [binder, in Coq.setoid_ring.Ncring]
T:554 [binder, in Coq.ssr.ssrbool]
t:558 [binder, in Coq.micromega.Tauto]
T:56 [binder, in Coq.ssr.ssreflect]
t:56 [binder, in Coq.Sets.Uniset]
t:563 [binder, in Coq.micromega.Tauto]
t:57 [binder, in Coq.Array.PArray]
t:57 [binder, in Coq.Sets.Multiset]
T:59 [binder, in Coq.rtauto.Bintree]
t:59 [binder, in Coq.MSets.MSetRBT]
t:595 [binder, in Coq.MSets.MSetRBT]
t:598 [binder, in Coq.MSets.MSetRBT]
t:60 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
T:60 [binder, in Coq.ssr.ssreflect]
t:603 [binder, in Coq.MSets.MSetRBT]
t:605 [binder, in Coq.MSets.MSetRBT]
T:607 [binder, in Coq.ssr.ssrbool]
t:607 [binder, in Coq.MSets.MSetRBT]
t:61 [binder, in Coq.Sets.Multiset]
t:61 [binder, in Coq.Sorting.Heap]
t:617 [binder, in Coq.MSets.MSetRBT]
t:618 [binder, in Coq.MSets.MSetRBT]
t:618 [binder, in Coq.micromega.Tauto]
t:62 [binder, in Coq.Array.PArray]
t:627 [binder, in Coq.micromega.Tauto]
T:63 [binder, in Coq.Logic.ChoiceFacts]
t:63 [binder, in Coq.Sets.Uniset]
t:632 [binder, in Coq.micromega.Tauto]
T:64 [binder, in Coq.setoid_ring.Ncring]
T:640 [binder, in Coq.micromega.Tauto]
t:65 [binder, in Coq.Array.PArray]
T:65 [binder, in Coq.ssr.ssreflect]
t:65 [binder, in Coq.MSets.MSetRBT]
t:66 [binder, in Coq.nsatz.NsatzTactic]
t:66 [binder, in Coq.Sets.Multiset]
T:67 [binder, in Coq.ssr.ssreflect]
t:67 [binder, in Coq.Sets.Uniset]
T:67 [binder, in Coq.Sorting.Heap]
T:670 [binder, in Coq.ssr.ssrbool]
T:675 [binder, in Coq.ssr.ssrbool]
T:68 [binder, in Coq.rtauto.Bintree]
T:681 [binder, in Coq.ssr.ssrbool]
T:688 [binder, in Coq.ssr.ssrbool]
T:696 [binder, in Coq.ssr.ssrbool]
t:7 [binder, in Coq.setoid_ring.Ncring_tac]
t:7 [binder, in Coq.Reals.RiemannInt]
T:7 [binder, in Coq.micromega.DeclConstant]
t:7 [binder, in Coq.MSets.MSetGenTree]
T:70 [binder, in Coq.ssr.ssreflect]
t:71 [binder, in Coq.Sets.Uniset]
T:72 [binder, in Coq.Sorting.Heap]
T:73 [binder, in Coq.ssr.ssreflect]
T:74 [binder, in Coq.Logic.ChoiceFacts]
t:74 [binder, in Coq.MSets.MSetRBT]
t:76 [binder, in Coq.Sets.Uniset]
t:76 [binder, in Coq.Vectors.VectorDef]
t:77 [binder, in Coq.MSets.MSetRBT]
t:77 [binder, in Coq.Reals.Ratan]
T:77 [binder, in Coq.Sorting.Heap]
T:78 [binder, in Coq.micromega.ZifyClasses]
T:79 [binder, in Coq.Sorting.Heap]
t:8 [binder, in Coq.Array.PArray]
T:84 [binder, in Coq.Sorting.Heap]
T:87 [binder, in Coq.Logic.ChoiceFacts]
T:88 [binder, in Coq.micromega.ZifyClasses]
t:93 [binder, in Coq.Vectors.VectorDef]
t:94 [binder, in Coq.micromega.ZMicromega]
T:97 [binder, in Coq.ssr.ssrfun]
t:99 [binder, in Coq.Vectors.VectorDef]
| 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 | (70451 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 | (1003 entries) |
| Binder 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 | (45703 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 | (771 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 | (1516 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 | (579 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 | (11670 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 | (1018 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 | (622 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 | (304 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 | (472 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 | (482 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 | (844 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 | (1187 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 | (4117 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 | (163 entries) |