| 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 | (86 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 | (2 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 | (30 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 | (36 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 | (16 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 | (2 entries) |
Global Index
A
A [constructor, in HigmanCF.Higman2]A [constructor, in HigmanCF.Higman]
B
B [constructor, in HigmanCF.Higman2]B [constructor, in HigmanCF.Higman]
bar [inductive, in HigmanCF.Higman2]
bar [inductive, in HigmanCF.Higman]
bar_idx [lemma, in HigmanCF.Higman2]
bar1 [constructor, in HigmanCF.Higman2]
bar1 [constructor, in HigmanCF.Higman]
bar2 [constructor, in HigmanCF.Higman2]
bar2 [constructor, in HigmanCF.Higman]
E
emb [inductive, in HigmanCF.Higman2]emb [inductive, in HigmanCF.Higman]
emb0 [constructor, in HigmanCF.Higman2]
emb0 [constructor, in HigmanCF.Higman]
emb1 [constructor, in HigmanCF.Higman2]
emb1 [constructor, in HigmanCF.Higman]
emb2 [constructor, in HigmanCF.Higman2]
emb2 [constructor, in HigmanCF.Higman]
G
good [inductive, in HigmanCF.Higman2]good [inductive, in HigmanCF.Higman]
good_idx [lemma, in HigmanCF.Higman2]
good_prefix [lemma, in HigmanCF.Higman]
good_prefix_lemma [lemma, in HigmanCF.Higman]
good0 [constructor, in HigmanCF.Higman2]
good0 [constructor, in HigmanCF.Higman]
good1 [constructor, in HigmanCF.Higman2]
good1 [constructor, in HigmanCF.Higman]
H
higman [lemma, in HigmanCF.Higman2]higman [lemma, in HigmanCF.Higman]
Higman [library]
higman_idx [lemma, in HigmanCF.Higman2]
Higman2 [library]
I
is_prefix_cons [constructor, in HigmanCF.Higman2]is_prefix_nil [constructor, in HigmanCF.Higman2]
is_prefix [inductive, in HigmanCF.Higman2]
is_prefix_cons [constructor, in HigmanCF.Higman]
is_prefix_nil [constructor, in HigmanCF.Higman]
is_prefix [inductive, in HigmanCF.Higman]
L
L [inductive, in HigmanCF.Higman2]L [inductive, in HigmanCF.Higman]
lemma1 [lemma, in HigmanCF.Higman2]
lemma1 [lemma, in HigmanCF.Higman]
lemma2 [lemma, in HigmanCF.Higman2]
lemma2 [lemma, in HigmanCF.Higman]
lemma2' [lemma, in HigmanCF.Higman2]
lemma2' [lemma, in HigmanCF.Higman]
lemma3 [lemma, in HigmanCF.Higman2]
lemma3 [lemma, in HigmanCF.Higman]
lemma3' [lemma, in HigmanCF.Higman2]
lemma3' [lemma, in HigmanCF.Higman]
lemma4 [lemma, in HigmanCF.Higman2]
lemma4 [lemma, in HigmanCF.Higman]
letter [inductive, in HigmanCF.Higman2]
letter [inductive, in HigmanCF.Higman]
letter_eq_dec [lemma, in HigmanCF.Higman2]
letter_neq [lemma, in HigmanCF.Higman2]
letter_eq_dec [lemma, in HigmanCF.Higman]
letter_neq [lemma, in HigmanCF.Higman]
L_idx [lemma, in HigmanCF.Higman2]
L0 [constructor, in HigmanCF.Higman2]
L0 [constructor, in HigmanCF.Higman]
L1 [constructor, in HigmanCF.Higman2]
L1 [constructor, in HigmanCF.Higman]
P
prop1 [lemma, in HigmanCF.Higman2]prop1 [lemma, in HigmanCF.Higman]
prop2 [lemma, in HigmanCF.Higman2]
prop2 [lemma, in HigmanCF.Higman]
prop3 [lemma, in HigmanCF.Higman2]
prop3 [lemma, in HigmanCF.Higman]
R
R [inductive, in HigmanCF.Higman2]R [inductive, in HigmanCF.Higman]
R0 [constructor, in HigmanCF.Higman2]
R0 [constructor, in HigmanCF.Higman]
R1 [constructor, in HigmanCF.Higman2]
R1 [constructor, in HigmanCF.Higman]
T
T [inductive, in HigmanCF.Higman2]T [inductive, in HigmanCF.Higman]
T0 [constructor, in HigmanCF.Higman2]
T0 [constructor, in HigmanCF.Higman]
T1 [constructor, in HigmanCF.Higman2]
T1 [constructor, in HigmanCF.Higman]
T2 [constructor, in HigmanCF.Higman2]
T2 [constructor, in HigmanCF.Higman]
W
word [definition, in HigmanCF.Higman2]word [definition, in HigmanCF.Higman]
Library Index
H
HigmanHigman2
Lemma Index
B
bar_idx [in HigmanCF.Higman2]G
good_idx [in HigmanCF.Higman2]good_prefix [in HigmanCF.Higman]
good_prefix_lemma [in HigmanCF.Higman]
H
higman [in HigmanCF.Higman2]higman [in HigmanCF.Higman]
higman_idx [in HigmanCF.Higman2]
L
lemma1 [in HigmanCF.Higman2]lemma1 [in HigmanCF.Higman]
lemma2 [in HigmanCF.Higman2]
lemma2 [in HigmanCF.Higman]
lemma2' [in HigmanCF.Higman2]
lemma2' [in HigmanCF.Higman]
lemma3 [in HigmanCF.Higman2]
lemma3 [in HigmanCF.Higman]
lemma3' [in HigmanCF.Higman2]
lemma3' [in HigmanCF.Higman]
lemma4 [in HigmanCF.Higman2]
lemma4 [in HigmanCF.Higman]
letter_eq_dec [in HigmanCF.Higman2]
letter_neq [in HigmanCF.Higman2]
letter_eq_dec [in HigmanCF.Higman]
letter_neq [in HigmanCF.Higman]
L_idx [in HigmanCF.Higman2]
P
prop1 [in HigmanCF.Higman2]prop1 [in HigmanCF.Higman]
prop2 [in HigmanCF.Higman2]
prop2 [in HigmanCF.Higman]
prop3 [in HigmanCF.Higman2]
prop3 [in HigmanCF.Higman]
Constructor Index
A
A [in HigmanCF.Higman2]A [in HigmanCF.Higman]
B
B [in HigmanCF.Higman2]B [in HigmanCF.Higman]
bar1 [in HigmanCF.Higman2]
bar1 [in HigmanCF.Higman]
bar2 [in HigmanCF.Higman2]
bar2 [in HigmanCF.Higman]
E
emb0 [in HigmanCF.Higman2]emb0 [in HigmanCF.Higman]
emb1 [in HigmanCF.Higman2]
emb1 [in HigmanCF.Higman]
emb2 [in HigmanCF.Higman2]
emb2 [in HigmanCF.Higman]
G
good0 [in HigmanCF.Higman2]good0 [in HigmanCF.Higman]
good1 [in HigmanCF.Higman2]
good1 [in HigmanCF.Higman]
I
is_prefix_cons [in HigmanCF.Higman2]is_prefix_nil [in HigmanCF.Higman2]
is_prefix_cons [in HigmanCF.Higman]
is_prefix_nil [in HigmanCF.Higman]
L
L0 [in HigmanCF.Higman2]L0 [in HigmanCF.Higman]
L1 [in HigmanCF.Higman2]
L1 [in HigmanCF.Higman]
R
R0 [in HigmanCF.Higman2]R0 [in HigmanCF.Higman]
R1 [in HigmanCF.Higman2]
R1 [in HigmanCF.Higman]
T
T0 [in HigmanCF.Higman2]T0 [in HigmanCF.Higman]
T1 [in HigmanCF.Higman2]
T1 [in HigmanCF.Higman]
T2 [in HigmanCF.Higman2]
T2 [in HigmanCF.Higman]
Inductive Index
B
bar [in HigmanCF.Higman2]bar [in HigmanCF.Higman]
E
emb [in HigmanCF.Higman2]emb [in HigmanCF.Higman]
G
good [in HigmanCF.Higman2]good [in HigmanCF.Higman]
I
is_prefix [in HigmanCF.Higman2]is_prefix [in HigmanCF.Higman]
L
L [in HigmanCF.Higman2]L [in HigmanCF.Higman]
letter [in HigmanCF.Higman2]
letter [in HigmanCF.Higman]
R
R [in HigmanCF.Higman2]R [in HigmanCF.Higman]
T
T [in HigmanCF.Higman2]T [in HigmanCF.Higman]
Definition Index
W
word [in HigmanCF.Higman2]word [in HigmanCF.Higman]
| 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 | (86 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 | (2 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 | (30 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 | (36 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 | (16 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 | (2 entries) |