| 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 | (75519 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 | (245 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 | (61331 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 | (144 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 | (89 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 | (236 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 | (6913 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 | (1141 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 | (34 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 | (269 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 | (443 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 | (296 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 | (604 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 | (248 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 | (3386 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 | (140 entries) |
O (instance)
OnOne2_local_env_length [in MetaCoq.PCUIC.utils.PCUICOnOne]on_ctx_free_vars_proper_pointwise [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_ctx_free_vars_proper [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx_proper [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_decl_proper_pointwise [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_decl_proper [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_proper_pointwise [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_proper [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_terms_proper [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
optimized_abstract_env_prop [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
optimized_abstract_env_ext_prop [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
optimized_abstract_env_struct [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
optimized_abstract_env_ext_struct [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
option_UIP [in MetaCoq.PCUIC.PCUICWcbvEval]
option_map_proper [in MetaCoq.Template.utils.MCOption]
option_monad_exc [in MetaCoq.Template.monad_utils]
option_monad [in MetaCoq.Template.monad_utils]
orP_Proper [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
orP_Proper [in MetaCoq.Template.utils.MCPred]