| 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 | (18986 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 | (228 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 | (297 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 | (1273 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 | (313 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 | (8135 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 | (1490 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 | (52 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 | (343 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 | (524 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 | (720 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 | (401 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 | (331 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 | (4701 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 | (178 entries) |
P (instance)
PCUICEnvironmentDecide.constant_body_eq_dec [in MetaRocq.PCUIC.Syntax.PCUICReflect]PCUICEnvironmentDecide.constructor_body_eq_dec [in MetaRocq.PCUIC.Syntax.PCUICReflect]
PCUICEnvironmentDecide.context_eq_dec [in MetaRocq.PCUIC.Syntax.PCUICReflect]
PCUICEnvironmentDecide.global_decl_eq_dec [in MetaRocq.PCUIC.Syntax.PCUICReflect]
PCUICEnvironmentDecide.mutual_inductive_body_eq_dec [in MetaRocq.PCUIC.Syntax.PCUICReflect]
PCUICEnvironmentDecide.one_inductive_body_eq_dec [in MetaRocq.PCUIC.Syntax.PCUICReflect]
PCUICEnvironmentDecide.projection_body_eq_dec [in MetaRocq.PCUIC.Syntax.PCUICReflect]
PCUICTermDecide.term_eq_dec [in MetaRocq.PCUIC.Syntax.PCUICReflect]
pointwise_subrelation2 [in MetaRocq.Utils.MRPrelude]
pointwise_subrelation [in MetaRocq.Utils.MRPrelude]
PolymorphicInstances.quote_relax_universe [in MetaRocq.Quotation.ToPCUIC.Init]
PolymorphicInstances.quote_relax_universe [in MetaRocq.Quotation.ToTemplate.Init]
predicate_eq_dec [in MetaRocq.Template.Ast]
pred_of_simpl_proper [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
pred1_rel_refl [in MetaRocq.PCUIC.PCUICConfluence]
pred1_refl [in MetaRocq.PCUIC.PCUICConfluence]
pres_let_bodies_trans [in MetaRocq.PCUIC.PCUICRedTypeIrrelevance]
pres_let_bodies_refl [in MetaRocq.PCUIC.PCUICRedTypeIrrelevance]
prim_tag_model_eqdec [in MetaRocq.Erasure.EPrimitive]
prim_val_reflect_eq [in MetaRocq.Erasure.EPrimitive]
prim_model_eqdec [in MetaRocq.Erasure.EPrimitive]
prim_model_reflecteq [in MetaRocq.Erasure.EPrimitive]
prim_tag_model_eqdec [in MetaRocq.PCUIC.utils.PCUICPrimitive]
prim_val_reflect_eq [in MetaRocq.PCUIC.utils.PCUICPrimitive]
prim_model_eqdec [in MetaRocq.PCUIC.utils.PCUICPrimitive]
prim_model_reflecteq [in MetaRocq.PCUIC.utils.PCUICPrimitive]
Prod_reflexivity [in MetaRocq.Utils.MRProd]
proper_map_ho [in MetaRocq.Utils.MRList]
proper_sort_sup_eq_sort [in MetaRocq.Common.Universes]
proper_univ_sup_eq_univ [in MetaRocq.Common.Universes]
proper_pair_levels_gcs [in MetaRocq.Erasure.ErasureFunction]
Proper_weaken_env_prop_full_gen_respectful [in MetaRocq.PCUIC.PCUICWeakeningEnv]
Proper_weaken_env_prop_gen_respectful [in MetaRocq.PCUIC.PCUICWeakeningEnv]
proper_red_ctx [in MetaRocq.PCUIC.PCUICConfluence]
proper_inst' [in MetaRocq.PCUIC.PCUICSigmaCalculus]
proper_inst [in MetaRocq.PCUIC.PCUICSigmaCalculus]
proper_add_le_l [in MetaRocq.Utils.MRArith]
proper_add_le_r [in MetaRocq.Utils.MRArith]
proper_S_le [in MetaRocq.Utils.MRArith]
proper_add_lt_l [in MetaRocq.Utils.MRArith]
proper_add_lt_r [in MetaRocq.Utils.MRArith]
proper_S_lt [in MetaRocq.Utils.MRArith]
proper_add_level_edges' [in MetaRocq.SafeChecker.PCUICSafeChecker]
proper_add_uctx [in MetaRocq.SafeChecker.PCUICSafeChecker]
proper_add_level_edges [in MetaRocq.SafeChecker.PCUICSafeChecker]
proper_add_level_edges' [in MetaRocq.Common.uGraph]
proper_add_uctx [in MetaRocq.Common.uGraph]
proper_add_level_edges [in MetaRocq.Common.uGraph]
proper_pair_levels_gcs [in MetaRocq.Common.uGraph]
proper_ext_eq [in MetaRocq.Utils.MRPrelude]
PropLevel.lt_strorder [in MetaRocq.Common.Universes]
| 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 | (18986 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 | (228 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 | (297 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 | (1273 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 | (313 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 | (8135 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 | (1490 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 | (52 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 | (343 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 | (524 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 | (720 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 | (401 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 | (331 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 | (4701 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 | (178 entries) |