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 | (69918 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 | (997 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 | (45430 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 | (770 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 | (576 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 | (11559 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 | (981 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 | (299 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 | (466 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 | (812 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 | (1156 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 | (4086 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) |

## R (abbreviation)

R [in Coq.Reals.Rdefinitions]Raw.eqk [in Coq.FSets.FMapWeakList]

Raw.eqk [in Coq.FSets.FMapList]

Raw.eqke [in Coq.FSets.FMapWeakList]

Raw.eqke [in Coq.FSets.FMapList]

Raw.In [in Coq.FSets.FMapWeakList]

Raw.In [in Coq.FSets.FMapList]

Raw.Inf [in Coq.FSets.FMapList]

Raw.int [in Coq.FSets.FMapAVL]

Raw.ltk [in Coq.FSets.FMapList]

Raw.MapsTo [in Coq.FSets.FMapWeakList]

Raw.MapsTo [in Coq.FSets.FMapList]

Raw.NoDupA [in Coq.FSets.FMapWeakList]

Raw.oee' [in Coq.FSets.FMapWeakList]

Raw.oee' [in Coq.FSets.FMapList]

Raw.Proofs.eqk [in Coq.FSets.FMapAVL]

Raw.Proofs.eqke [in Coq.FSets.FMapAVL]

Raw.Proofs.ltk [in Coq.FSets.FMapAVL]

Raw.Proofs.map2_opt [in Coq.FSets.FMapAVL]

Raw.Sort [in Coq.FSets.FMapList]

Raw.t [in Coq.FSets.FMapAVL]

Raw.t [in Coq.FSets.FMapAVL]

reflect [in Coq.ssr.ssrbool]

ReflectF [in Coq.ssr.ssrbool]

ReflectT [in Coq.ssr.ssrbool]

refl_id [in Coq.Init.Logic_Type]

refl_equal [in Coq.Init.Logic]

RefutablePropositionExtensionality [in Coq.Logic.PropExtensionalityFacts]

RelationalChoice [in Coq.Logic.ChoiceFacts]

RepresentativeFunctionalChoice [in Coq.Logic.ChoiceFacts]

representative_boolean_partition [in Coq.Logic.ClassicalFacts]

rev_acc_rev [in Coq.Lists.List]

rev_acc [in Coq.Lists.List]

Rext [in Coq.setoid_ring.RealField]

right [in Coq.setoid_ring.Field_theory]

ring_correct [in Coq.setoid_ring.Field_theory]

ring_rw_pow_correct [in Coq.setoid_ring.Field_theory]

ring_rw_correct [in Coq.setoid_ring.Field_theory]

Rinv [in Coq.Reals.Rdefinitions]

Rlength [in Coq.Reals.RList]

Rlist [in Coq.Reals.RList]

Rlt [in Coq.Reals.Rdefinitions]

RmaxLess1 [in Coq.Reals.Rbasic_fun]

RmaxLess2 [in Coq.Reals.Rbasic_fun]

RmaxSym [in Coq.Reals.Rbasic_fun]

Rmin_2 [in Coq.Reals.Ranalysis2]

Rmin_pos [in Coq.Reals.Ranalysis2]

Rmult [in Coq.Reals.Rdefinitions]

Ropp [in Coq.Reals.Rdefinitions]

Rplus [in Coq.Reals.Rdefinitions]

Rplus_lt_pos [in Coq.Reals.DiscrR]

Rset [in Coq.setoid_ring.RealField]

rtn1_trans_equiv [in Coq.Relations.Operators_Properties]

rtn1_trans [in Coq.Relations.Operators_Properties]

rtsn1_sym [in Coq.Relations.Operators_Properties]

rtsn1_trans [in Coq.Relations.Operators_Properties]

rtsn1_rts [in Coq.Relations.Operators_Properties]

rtsn1_trans [in Coq.Relations.Relation_Operators]

rtsn1_refl [in Coq.Relations.Relation_Operators]

rts_rtsn1_equiv [in Coq.Relations.Operators_Properties]

rts_rtsn1 [in Coq.Relations.Operators_Properties]

rts_rts1n_equiv [in Coq.Relations.Operators_Properties]

rts_rts1n [in Coq.Relations.Operators_Properties]

rts_1n_trans [in Coq.Relations.Operators_Properties]

rts1n_sym [in Coq.Relations.Operators_Properties]

rts1n_rts [in Coq.Relations.Operators_Properties]

rts1n_trans [in Coq.Relations.Relation_Operators]

rts1n_refl [in Coq.Relations.Relation_Operators]

rt1n_trans_equiv [in Coq.Relations.Operators_Properties]

rt1n_trans [in Coq.Relations.Operators_Properties]

R_rt1n [in Coq.Relations.Operators_Properties]

R_rtn1 [in Coq.Relations.Operators_Properties]

R0 [in Coq.Reals.Rdefinitions]

R1 [in Coq.Reals.Rdefinitions]

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 | (69918 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 | (997 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 | (45430 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 | (770 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 | (576 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 | (11559 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 | (981 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 | (299 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 | (466 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 | (812 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 | (1156 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 | (4086 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) |