F (Global Index)
| Files | 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 | _ |
| Definitions | 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 | _ |
| Lemmas | 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 | _ |
| Abbreviations | 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 | _ |
| 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 | _ |
| Notations |
F
f0 [ax, in T.Amida]f1 [ax, in T.Amida]
f2 [ax, in T.Amida]
f3 [ax, in T.Amida]
Fin [mod, in T.Common]
Fin.le [def, in T.Common]
Fin.le_dec [def, in T.Common]
Fin.le_succ_l [prf, in T.Common]
Fin.lt [def, in T.Common]
Fin.lt_dec [def, in T.Common]
Fin.lt_le_incl [prf, in T.Common]
Fin.lt_to_nat [prf, in T.Common]
Fin.succ_opt [def, in T.Common]
Fin.succ_opt_inj [prf, in T.Common]
Fin.succ_opt_None [prf, in T.Common]
Fin.succ_opt_S [prf, in T.Common]
Fin.succ_opt_to_nat [prf, in T.Common]
Fin.to_nat [def, in T.Common]
Fin.to_nat_inj [prf, in T.Common]
Finished [def, in T.Amida]
Finished_dec [def, in T.Amida]