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 | (72679 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 | (1040 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 | (47172 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 | (791 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 | (1553 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 | (585 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 | (11862 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 | (1030 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 | (625 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 | (308 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 | (474 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 | (493 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 | (896 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 | (1443 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 | (4242 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 | (165 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 [abbreviation, in Coq.Numbers.Cyclic.Int63.Int63]

tail0 [axiom, in Coq.Numbers.Cyclic.Int63.PrimInt63]

tail0 [abbreviation, in Coq.Numbers.Cyclic.Int63.Uint63]

tail0_spec [abbreviation, in Coq.Numbers.Cyclic.Int63.Int63]

tail0_spec [axiom, in Coq.Numbers.Cyclic.Int63.Uint63]

tail00_spec [abbreviation, in Coq.Numbers.Cyclic.Int63.Int63]

tail00_spec [lemma, in Coq.Numbers.Cyclic.Int63.Uint63]

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':108 [binder, in Coq.micromega.Tauto]

TA:107 [binder, in Coq.micromega.Tauto]

TA:6 [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:353 [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:210 [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:436 [binder, in Coq.micromega.Tauto]

tg:440 [binder, in Coq.micromega.Tauto]

tg:562 [binder, in Coq.micromega.Tauto]

tg:567 [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:378 [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:287 [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_Forall2 [lemma, in Coq.Vectors.VectorSpec]

to_list_In [lemma, in Coq.Vectors.VectorSpec]

to_list_Exists [lemma, in Coq.Vectors.VectorSpec]

to_list_Forall [lemma, in Coq.Vectors.VectorSpec]

to_list_fold_right [lemma, in Coq.Vectors.VectorSpec]

to_list_fold_left [lemma, in Coq.Vectors.VectorSpec]

to_list_map [lemma, in Coq.Vectors.VectorSpec]

to_list_rev [lemma, in Coq.Vectors.VectorSpec]

to_list_rev_append [lemma, in Coq.Vectors.VectorSpec]

to_list_rev_append_tail [lemma, in Coq.Vectors.VectorSpec]

to_list_append [lemma, in Coq.Vectors.VectorSpec]

to_list_tl [lemma, in Coq.Vectors.VectorSpec]

to_list_nth_order [lemma, in Coq.Vectors.VectorSpec]

to_list_const [lemma, in Coq.Vectors.VectorSpec]

to_list_last [lemma, in Coq.Vectors.VectorSpec]

to_list_hd [lemma, in Coq.Vectors.VectorSpec]

to_list_cons [lemma, in Coq.Vectors.VectorSpec]

to_list_nil [lemma, in Coq.Vectors.VectorSpec]

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 [abbreviation, in Coq.Numbers.Cyclic.Int63.Int63]

to_Z_gcd [abbreviation, in Coq.Numbers.Cyclic.Int63.Int63]

to_Z_inj [abbreviation, in Coq.Numbers.Cyclic.Int63.Int63]

to_Z_1 [abbreviation, in Coq.Numbers.Cyclic.Int63.Int63]

to_Z_0 [abbreviation, in Coq.Numbers.Cyclic.Int63.Int63]

to_Z_bounded [abbreviation, in Coq.Numbers.Cyclic.Int63.Int63]

to_Z_rec_bounded [abbreviation, in Coq.Numbers.Cyclic.Int63.Int63]

to_Z [abbreviation, in Coq.Numbers.Cyclic.Int63.Int63]

to_Z_rec [abbreviation, 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 [abbreviation, in Coq.micromega.ZifyInt63]

to_nat_non_decreasing [lemma, in Coq.Arith.Cantor]

to_nat_spec2 [lemma, in Coq.Arith.Cantor]

to_nat_spec [lemma, in Coq.Arith.Cantor]

to_nat_inj [lemma, in Coq.Arith.Cantor]

to_nat [definition, in Coq.Arith.Cantor]

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_Z_bounded [lemma, in Coq.micromega.ZifySint63]

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_Z_bounded [lemma, in Coq.micromega.ZifyUint63]

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_Z_split [lemma, in Coq.Numbers.Cyclic.Int63.Uint63]

to_Z_gcd [lemma, in Coq.Numbers.Cyclic.Int63.Uint63]

to_Z_inj [lemma, in Coq.Numbers.Cyclic.Int63.Uint63]

to_Z_1 [lemma, in Coq.Numbers.Cyclic.Int63.Uint63]

to_Z_0 [lemma, in Coq.Numbers.Cyclic.Int63.Uint63]

to_Z_bounded [lemma, in Coq.Numbers.Cyclic.Int63.Uint63]

to_Z_rec_bounded [lemma, in Coq.Numbers.Cyclic.Int63.Uint63]

to_Z [definition, in Coq.Numbers.Cyclic.Int63.Uint63]

to_Z_rec [definition, in Coq.Numbers.Cyclic.Int63.Uint63]

to_constr:294 [binder, in Coq.micromega.Tauto]

to_constrT [record, in Coq.micromega.Tauto]

to_Z_abs [lemma, in Coq.Numbers.Cyclic.Int63.Sint63]

to_Z_opp [lemma, in Coq.Numbers.Cyclic.Int63.Sint63]

to_Z_pred [lemma, in Coq.Numbers.Cyclic.Int63.Sint63]

to_Z_succ [lemma, in Coq.Numbers.Cyclic.Int63.Sint63]

to_Z_mul [lemma, in Coq.Numbers.Cyclic.Int63.Sint63]

to_Z_sub [lemma, in Coq.Numbers.Cyclic.Int63.Sint63]

to_Z_add [lemma, in Coq.Numbers.Cyclic.Int63.Sint63]

to_Z_cmodwB [lemma, in Coq.Numbers.Cyclic.Int63.Sint63]

to_Z_mod_Uint63to_Z [lemma, in Coq.Numbers.Cyclic.Int63.Sint63]

to_Z_inj [lemma, in Coq.Numbers.Cyclic.Int63.Sint63]

to_Z_bounded [lemma, in Coq.Numbers.Cyclic.Int63.Sint63]

to_Z_max [lemma, in Coq.Numbers.Cyclic.Int63.Sint63]

to_Z_min [lemma, in Coq.Numbers.Cyclic.Int63.Sint63]

to_Z_0 [lemma, in Coq.Numbers.Cyclic.Int63.Sint63]

to_Z [definition, in Coq.Numbers.Cyclic.Int63.Sint63]

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]

Trace [abbreviation, in Coq.micromega.Tauto]

Trace [inductive, in Coq.micromega.Tauto]

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:514 [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:109 [binder, in Coq.micromega.Tauto]

TX:151 [binder, in Coq.micromega.Tauto]

TX:161 [binder, in Coq.micromega.Tauto]

TX:180 [binder, in Coq.micromega.ZMicromega]

TX:183 [binder, in Coq.micromega.Tauto]

TX:188 [binder, in Coq.micromega.Tauto]

TX:193 [binder, in Coq.micromega.Tauto]

TX:237 [binder, in Coq.micromega.Tauto]

TX:267 [binder, in Coq.micromega.Tauto]

tx:28 [binder, in Coq.Reals.Rgeom]

tx:37 [binder, in Coq.Reals.Rgeom]

TX:456 [binder, in Coq.micromega.Tauto]

TX:466 [binder, in Coq.micromega.Tauto]

TX:476 [binder, in Coq.micromega.Tauto]

TX:486 [binder, in Coq.micromega.Tauto]

TX:496 [binder, in Coq.micromega.Tauto]

tx:63 [binder, in Coq.Reals.Rgeom]

TX:7 [binder, in Coq.micromega.Tauto]

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':224 [binder, in Coq.micromega.Tauto]

t':248 [binder, in Coq.micromega.Tauto]

t':254 [binder, in Coq.micromega.Tauto]

t':260 [binder, in Coq.micromega.Tauto]

t':266 [binder, in Coq.micromega.Tauto]

t':509 [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:70 [binder, in Coq.Sorting.Heap]

T1:71 [binder, in Coq.micromega.ZifyClasses]

T1:722 [binder, in Coq.ssr.ssrbool]

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:731 [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: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:130 [binder, in Coq.micromega.Tauto]

t:131 [binder, in Coq.Vectors.VectorDef]

T:132 [binder, in Coq.Classes.RelationClasses]

T:134 [binder, in Coq.ssr.ssrbool]

T:136 [binder, in Coq.ssr.ssrfun]

t:137 [binder, in Coq.Reals.MVT]

t:138 [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:142 [binder, in Coq.micromega.Tauto]

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: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:198 [binder, in Coq.MSets.MSetRBT]

T:2 [binder, in Coq.micromega.ZifyClasses]

t:2 [binder, in Coq.setoid_ring.Ncring_tac]

t:200 [binder, in Coq.micromega.Tauto]

t:208 [binder, in Coq.micromega.Tauto]

t:21 [binder, in Coq.Reals.RiemannInt]

t:21 [binder, in Coq.Program.Equality]

t:214 [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:221 [binder, in Coq.Reals.RiemannInt]

t:222 [binder, in Coq.micromega.Tauto]

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:249 [binder, in Coq.micromega.RingMicromega]

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:260 [binder, in Coq.micromega.RingMicromega]

t:261 [binder, in Coq.micromega.RingMicromega]

T:261 [binder, in Coq.ssr.ssrbool]

T:262 [binder, in Coq.ssr.ssrbool]

t:263 [binder, in Coq.micromega.ZMicromega]

T:264 [binder, in Coq.micromega.RingMicromega]

t:265 [binder, in Coq.micromega.RingMicromega]

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.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:276 [binder, in Coq.Init.Logic]

t:277 [binder, in Coq.micromega.RingMicromega]

t:277 [binder, in Coq.micromega.ZMicromega]

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:280 [binder, in Coq.ssr.ssrbool]

t:281 [binder, in Coq.micromega.RingMicromega]

t:284 [binder, in Coq.Reals.RiemannInt]

T:284 [binder, in Coq.ssr.ssrbool]

t:287 [binder, in Coq.Reals.RiemannInt]

T:289 [binder, in Coq.ssr.ssrbool]

t:29 [binder, in Coq.Sets.Permut]

T:290 [binder, in Coq.ssr.ssrbool]

T:291 [binder, in Coq.ssr.ssrbool]

t:292 [binder, in Coq.Reals.RiemannInt]

T:292 [binder, in Coq.ssr.ssrbool]

T:294 [binder, in Coq.ssr.ssrbool]

t:295 [binder, in Coq.Reals.RiemannInt]

T:295 [binder, in Coq.ssr.ssrbool]

T:296 [binder, in Coq.ssr.ssrbool]

t:298 [binder, in Coq.QArith.QArith_base]

T:299 [binder, in Coq.ssr.ssrbool]

t:3 [binder, in Coq.Numbers.Cyclic.Int31.Int31]

T:30 [binder, in Coq.ssr.ssrfun]

T:302 [binder, in Coq.ssr.ssrbool]

t:302 [binder, in Coq.QArith.QArith_base]

T:304 [binder, in Coq.ssr.ssrbool]

t:307 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

t:308 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

t:309 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

t:310 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

t:311 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

T:315 [binder, in Coq.ssr.ssrbool]

T:317 [binder, in Coq.ssr.ssrbool]

t:318 [binder, in Coq.Reals.RiemannInt]

T:318 [binder, in Coq.ssr.ssrbool]

t:318 [binder, in Coq.QArith.QArith_base]

t:32 [binder, in Coq.Reals.RiemannInt]

T:32 [binder, in Coq.ssr.ssreflect]

T:320 [binder, in Coq.ssr.ssrbool]

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:327 [binder, in Coq.ssr.ssrbool]

T:328 [binder, in Coq.ssr.ssrbool]

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:339 [binder, in Coq.ssr.ssrbool]

t:34 [binder, in Coq.omega.OmegaLemmas]

T:342 [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:351 [binder, in Coq.QArith.QArith_base]

T:353 [binder, in Coq.ssr.ssrbool]

t:355 [binder, in Coq.Reals.RiemannInt]

t:355 [binder, in Coq.QArith.QArith_base]

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:359 [binder, in Coq.QArith.QArith_base]

T:362 [binder, in Coq.ssr.ssrbool]

t:363 [binder, in Coq.Reals.RiemannInt]

T:365 [binder, in Coq.ssr.ssrbool]

t:366 [binder, in Coq.Reals.RiemannInt]

T:366 [binder, in Coq.ssr.ssrbool]

t:369 [binder, in Coq.Reals.RiemannInt]

T:369 [binder, in Coq.ssr.ssrbool]

T:37 [binder, in Coq.setoid_ring.Ncring]

t:370 [binder, in Coq.micromega.Tauto]

t:372 [binder, in Coq.Reals.RiemannInt]

T:373 [binder, in Coq.ssr.ssrbool]

T:377 [binder, in Coq.ssr.ssrbool]

t:378 [binder, in Coq.micromega.ZMicromega]

T:380 [binder, in Coq.ssr.ssrbool]

T:382 [binder, in Coq.ssr.ssrbool]

t:387 [binder, in Coq.micromega.Tauto]

t:388 [binder, in Coq.Reals.RiemannInt]

t:391 [binder, in Coq.ssr.ssrfun]

t:392 [binder, in Coq.micromega.Tauto]

t:393 [binder, in Coq.Reals.RiemannInt]

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:402 [binder, in Coq.MSets.MSetRBT]

T:405 [binder, in Coq.ssr.ssrbool]

T:406 [binder, in Coq.ssr.ssrbool]

T:407 [binder, in Coq.ssr.ssrbool]

t:408 [binder, in Coq.Reals.RiemannInt]

T:409 [binder, in Coq.ssr.ssrbool]

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:45 [binder, in Coq.Array.PArray]

t:45 [binder, in Coq.Sets.Permut]

T:454 [binder, in Coq.ssr.ssrbool]

T:458 [binder, in Coq.ssr.ssrbool]

t:46 [binder, in Coq.Sets.Multiset]

T:46 [binder, in Coq.setoid_ring.Ncring]

T:463 [binder, in Coq.ssr.ssrbool]

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: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:493 [binder, in Coq.ssr.ssrbool]

T:497 [binder, in Coq.ssr.ssrbool]

T:5 [binder, in Coq.ssr.ssrfun]

T:50 [binder, in Coq.Sorting.Heap]

t:505 [binder, in Coq.micromega.Tauto]

t:508 [binder, in Coq.micromega.Tauto]

T:511 [binder, in Coq.ssr.ssrbool]

T:519 [binder, in Coq.ssr.ssrbool]

t:52 [binder, in Coq.Reals.RiemannInt]

T:529 [binder, in Coq.ssr.ssrbool]

t:53 [binder, in Coq.Sets.Multiset]

t:531 [binder, in Coq.micromega.Tauto]

t:539 [binder, in Coq.micromega.Tauto]

T:55 [binder, in Coq.ssr.ssrbool]

T:55 [binder, in Coq.setoid_ring.Ncring]

t:55 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

T:56 [binder, in Coq.ssr.ssreflect]

t:56 [binder, in Coq.Sets.Uniset]

T:560 [binder, in Coq.ssr.ssrbool]

t:561 [binder, in Coq.micromega.Tauto]

t:566 [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.ssr.ssreflect]

t:603 [binder, in Coq.MSets.MSetRBT]

t:605 [binder, in Coq.MSets.MSetRBT]

t:607 [binder, in Coq.MSets.MSetRBT]

t:61 [binder, in Coq.Sets.Multiset]

t:61 [binder, in Coq.Sorting.Heap]

T:613 [binder, in Coq.ssr.ssrbool]

t:617 [binder, in Coq.MSets.MSetRBT]

t:618 [binder, in Coq.MSets.MSetRBT]

t:62 [binder, in Coq.Array.PArray]

t:621 [binder, in Coq.micromega.Tauto]

T:63 [binder, in Coq.Logic.ChoiceFacts]

t:63 [binder, in Coq.Sets.Uniset]

t:630 [binder, in Coq.micromega.Tauto]

t:635 [binder, in Coq.micromega.Tauto]

T:64 [binder, in Coq.setoid_ring.Ncring]

T:643 [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:68 [binder, in Coq.rtauto.Bintree]

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:712 [binder, in Coq.ssr.ssrbool]

T:717 [binder, in Coq.ssr.ssrbool]

T:72 [binder, in Coq.Sorting.Heap]

T:723 [binder, in Coq.ssr.ssrbool]

T:73 [binder, in Coq.ssr.ssreflect]

T:730 [binder, in Coq.ssr.ssrbool]

T:738 [binder, in Coq.ssr.ssrbool]

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 | (72679 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 | (1040 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 | (47172 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 | (791 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 | (1553 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 | (585 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 | (11862 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 | (1030 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 | (625 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 | (308 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 | (474 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 | (493 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 | (896 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 | (1443 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 | (4242 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 | (165 entries) |