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) |

## A (constructor)

Abort [in MetaCoq.Examples.tauto]abs_red_r [in MetaCoq.Template.Typing]

abs_red_l [in MetaCoq.Template.Typing]

abs_red_r [in MetaCoq.PCUIC.PCUICReduction]

abs_red_l [in MetaCoq.PCUIC.PCUICReduction]

ahyp [in MetaCoq.Erasure.EInduction]

all [in MetaCoq.Template.TemplateMonad.Common]

Alli_cons [in MetaCoq.Template.utils.All_Forall]

Alli_nil [in MetaCoq.Template.utils.All_Forall]

All_fold_cons [in MetaCoq.Template.utils.All_Forall]

All_fold_nil [in MetaCoq.Template.utils.All_Forall]

All_cons [in MetaCoq.Template.utils.All_Forall]

All_nil [in MetaCoq.Template.utils.All_Forall]

All2i_len_cons [in MetaCoq.Template.utils.All_Forall]

All2i_len_nil [in MetaCoq.Template.utils.All_Forall]

All2i_cons [in MetaCoq.Template.utils.All_Forall]

All2i_nil [in MetaCoq.Template.utils.All_Forall]

All2_fold_cons [in MetaCoq.Template.utils.All_Forall]

All2_fold_nil [in MetaCoq.Template.utils.All_Forall]

All2_cons [in MetaCoq.Template.utils.All_Forall]

All2_nil [in MetaCoq.Template.utils.All_Forall]

All3_cons [in MetaCoq.Template.utils.All_Forall]

All3_nil [in MetaCoq.Template.utils.All_Forall]

AlreadyDeclared [in MetaCoq.SafeChecker.PCUICErrors]

AlreadyDeclared [in MetaCoq.Template.Checker]

And [in MetaCoq.Examples.tauto]

app [in MetaCoq.Examples.add_constructor]

app_red_r [in MetaCoq.Template.Typing]

app_red_l [in MetaCoq.Template.Typing]

App_r [in MetaCoq.PCUIC.Syntax.PCUICPosition]

App_l [in MetaCoq.PCUIC.Syntax.PCUICPosition]

app_r [in MetaCoq.PCUIC.Syntax.PCUICPosition]

app_l [in MetaCoq.PCUIC.Syntax.PCUICPosition]

app_red_r [in MetaCoq.PCUIC.PCUICReduction]

app_red_l [in MetaCoq.PCUIC.PCUICReduction]

Args [in MetaCoq.SafeChecker.PCUICSafeConversion]

arity_spine_ass [in MetaCoq.PCUIC.PCUICSpine]

arity_spine_def [in MetaCoq.PCUIC.PCUICSpine]

arity_spine_conv [in MetaCoq.PCUIC.PCUICSpine]

arity_spine_nil [in MetaCoq.PCUIC.PCUICSpine]

assumption_context_vass [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]

assumption_context_nil [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]

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) |