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 | (3098 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 | (294 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 | (28 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 | (397 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 | (9 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 | (1414 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 | (80 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 | (7 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 | (35 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 | (35 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 | (135 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 | (84 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 | (555 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 | (25 entries) |

## U

unbump [definition, in Ssreflect.fintype]unbumpK [lemma, in Ssreflect.fintype]

unbumpKcond [lemma, in Ssreflect.fintype]

unbumpS [lemma, in Ssreflect.fintype]

unbump_addl [lemma, in Ssreflect.fintype]

undup [definition, in Ssreflect.seq]

undup_nil [lemma, in Ssreflect.seq]

undup_id [lemma, in Ssreflect.seq]

undup_uniq [lemma, in Ssreflect.seq]

unfold_in [lemma, in Ssreflect.ssrbool]

uniq [definition, in Ssreflect.seq]

uniq_perm_eq [lemma, in Ssreflect.seq]

uniq_size_uniq [lemma, in Ssreflect.seq]

uniq_leq_size [lemma, in Ssreflect.seq]

uniq_catCA [lemma, in Ssreflect.seq]

uniq_catC [lemma, in Ssreflect.seq]

unitE [lemma, in Ssreflect.ssrfun]

unit_countType [definition, in Ssreflect.choice]

unit_countMixin [definition, in Ssreflect.choice]

unit_choiceType [definition, in Ssreflect.choice]

unit_choiceMixin [definition, in Ssreflect.choice]

unit_eqType [definition, in Ssreflect.eqtype]

unit_eqMixin [definition, in Ssreflect.eqtype]

unit_eqP [lemma, in Ssreflect.eqtype]

unit_finType [definition, in Ssreflect.fintype]

unit_finMixin [definition, in Ssreflect.fintype]

unit_enumP [lemma, in Ssreflect.fintype]

unkeyed [abbreviation, in Ssreflect.ssreflect]

unkey_qualifier [projection, in Ssreflect.ssrbool]

unkey_pred [projection, in Ssreflect.ssrbool]

unless [definition, in Ssreflect.ssrbool]

unless_contra [lemma, in Ssreflect.ssrbool]

unlift [definition, in Ssreflect.fintype]

UnliftNone [constructor, in Ssreflect.fintype]

unliftP [lemma, in Ssreflect.fintype]

UnliftSome [constructor, in Ssreflect.fintype]

unlift_some [lemma, in Ssreflect.fintype]

unlift_none [lemma, in Ssreflect.fintype]

unlift_spec [inductive, in Ssreflect.fintype]

unlift_subproof [lemma, in Ssreflect.fintype]

unlock [lemma, in Ssreflect.ssreflect]

unlockable [record, in Ssreflect.ssreflect]

Unlockable [constructor, in Ssreflect.ssreflect]

unlocked [projection, in Ssreflect.ssreflect]

unlock_with [lemma, in Ssreflect.ssreflect]

unpickle [definition, in Ssreflect.choice]

unpickle_tagged [definition, in Ssreflect.choice]

unpickle_seq [definition, in Ssreflect.choice]

unsplit [definition, in Ssreflect.fintype]

unsplitK [lemma, in Ssreflect.fintype]

unwrap [projection, in Ssreflect.ssrfun]

unzip1 [definition, in Ssreflect.seq]

unzip1_zip [lemma, in Ssreflect.seq]

unzip2 [definition, in Ssreflect.seq]

unzip2_zip [lemma, in Ssreflect.seq]

uphalf [definition, in Ssreflect.ssrnat]

uphalf_half [lemma, in Ssreflect.ssrnat]

uphalf_double [lemma, in Ssreflect.ssrnat]

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 | (3098 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 | (294 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 | (28 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 | (397 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 | (9 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 | (1414 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 | (80 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 | (7 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 | (35 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 | (35 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 | (135 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 | (84 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 | (555 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 | (25 entries) |