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 | (73252 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 | (1016 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 | (47569 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 | (800 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 | (1555 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 | (592 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 | (11846 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 | (959 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 | (629 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 | (475 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 | (494 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 | (912 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 | (1503 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 | (4428 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 | (166 entries) |

## P (instance)

PairDecidableType.eq_equiv [in Coq.Structures.EqualitiesFacts]PairOrderedType.lt_compat [in Coq.Structures.OrdersEx]

PairOrderedType.lt_strorder [in Coq.Structures.OrdersEx]

PairUsualDecidableType.eq_equiv [in Coq.Structures.EqualitiesFacts]

pair_compat [in Coq.Classes.RelationPairs]

PartialOrder_proper [in Coq.Classes.Morphisms]

PartialOrder_proper_type [in Coq.Classes.CMorphisms]

partial_order_antisym [in Coq.Classes.RelationClasses]

partial_order_antisym [in Coq.Classes.CRelationClasses]

PEadd_ext [in Coq.setoid_ring.Field_theory]

PEmul_ext [in Coq.setoid_ring.Field_theory]

PEopp_ext [in Coq.setoid_ring.Field_theory]

PEpow_ext [in Coq.setoid_ring.Field_theory]

Pequiv_eq [in Coq.setoid_ring.Ring_polynom]

PermutationA_app [in Coq.Lists.SetoidPermutation]

PermutationA_cons [in Coq.Lists.SetoidPermutation]

Permutation_transp_equiv [in Coq.Sorting.Permutation]

Permutation_transp_sym [in Coq.Sorting.Permutation]

Permutation_list_max [in Coq.Sorting.Permutation]

Permutation_list_sum [in Coq.Sorting.Permutation]

Permutation_flat_map [in Coq.Sorting.Permutation]

Permutation_map' [in Coq.Sorting.Permutation]

Permutation_NoDup' [in Coq.Sorting.Permutation]

Permutation_Exists [in Coq.Sorting.Permutation]

Permutation_Forall [in Coq.Sorting.Permutation]

Permutation_length' [in Coq.Sorting.Permutation]

Permutation_rev' [in Coq.Sorting.Permutation]

Permutation_app' [in Coq.Sorting.Permutation]

Permutation_in' [in Coq.Sorting.Permutation]

Permutation_cons [in Coq.Sorting.Permutation]

Permutation_Equivalence [in Coq.Sorting.Permutation]

Permutation_refl' [in Coq.Sorting.Permutation]

PER_morphism [in Coq.Classes.Morphisms]

per_partial_app_morphism [in Coq.Classes.Morphisms]

PER_type_morphism [in Coq.Classes.CMorphisms]

per_partial_app_type_morphism [in Coq.Classes.CMorphisms]

PEsub_ext [in Coq.setoid_ring.Field_theory]

Pinj_ext [in Coq.setoid_ring.Ring_polynom]

pointwise_subrelation [in Coq.Classes.Morphisms]

pointwise_equivalence [in Coq.Classes.CEquivalence]

pointwise_transitive [in Coq.Classes.CEquivalence]

pointwise_symmetric [in Coq.Classes.CEquivalence]

pointwise_reflexive [in Coq.Classes.CEquivalence]

pointwise_subrelation [in Coq.Classes.CMorphisms]

pointwise_equivalence [in Coq.Classes.Equivalence]

pointwise_transitive [in Coq.Classes.Equivalence]

pointwise_symmetric [in Coq.Classes.Equivalence]

pointwise_reflexive [in Coq.Classes.Equivalence]

PositiveMap.eqke_equiv [in Coq.FSets.FMapPositive]

PositiveMap.eqk_equiv [in Coq.FSets.FMapPositive]

PositiveMap.ltk_strorder [in Coq.FSets.FMapPositive]

PositiveOrderedTypeBits.lt_strorder [in Coq.Structures.OrdersEx]

PositiveOrderedTypeBits.lt_compat [in Coq.Structures.OrdersEx]

PositiveSet.compare_compat [in Coq.MSets.MSetPositive]

PositiveSet.compare_compat_1 [in Coq.MSets.MSetPositive]

PositiveSet.eq_equiv [in Coq.MSets.MSetPositive]

PositiveSet.In_compat [in Coq.MSets.MSetPositive]

PositiveSet.lt_compat [in Coq.MSets.MSetPositive]

PositiveSet.lt_strorder [in Coq.MSets.MSetPositive]

Pos.le_partorder [in Coq.PArith.BinPos]

Pos.le_preorder [in Coq.PArith.BinPos]

Pos.lt_compat [in Coq.PArith.BinPos]

Pos.lt_strorder [in Coq.PArith.BinPos]

power_ring [in Coq.setoid_ring.Ncring]

pow_N_ext [in Coq.setoid_ring.Field_theory]

pow_ext [in Coq.setoid_ring.Field_theory]

Pphi_ext [in Coq.setoid_ring.Ring_polynom]

predicate_implication_preorder [in Coq.Classes.RelationClasses]

predicate_equivalence_equivalence [in Coq.Classes.RelationClasses]

prod_eqdec [in Coq.Classes.EquivDec]

prod_eqdec [in Coq.Classes.SetoidDec]

proper_proper [in Coq.Classes.Morphisms]

proper_subrelation_proper [in Coq.Classes.Morphisms]

proper_proper [in Coq.Classes.CMorphisms]

proper_subrelation_proper_arrow [in Coq.Classes.CMorphisms]

Props.bst_Ok [in Coq.MSets.MSetGenTree]

Props.empty_ok [in Coq.MSets.MSetGenTree]

Props.eq_equiv [in Coq.MSets.MSetGenTree]

Props.gt_tree_compat [in Coq.MSets.MSetGenTree]

Props.In_compat [in Coq.MSets.MSetGenTree]

Props.isok_Ok [in Coq.MSets.MSetGenTree]

Props.lt_compat [in Coq.MSets.MSetGenTree]

Props.lt_strorder [in Coq.MSets.MSetGenTree]

Props.lt_tree_compat [in Coq.MSets.MSetGenTree]

PX_ext [in Coq.setoid_ring.Ring_polynom]

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 | (73252 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 | (1016 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 | (47569 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 | (800 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 | (1555 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 | (592 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 | (11846 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 | (959 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 | (629 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 | (475 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 | (494 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 | (912 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 | (1503 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 | (4428 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 | (166 entries) |