| 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 |
_ |
(113 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 |
_ |
(72 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 |
_ |
(24 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 |
_ |
(8 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 |
_ |
(7 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 |
_ |
(2 entries) |
Global Index
A
Arrow [constructor, in Part1A]
B
Bind [constructor, in Binding]
Binding [library]
Bound [constructor, in Part1A]
C
cons_inDom [lemma, in Binding]
context [inductive, in Binding]
context [definition, in Part1A]
E
Empty [constructor, in Binding]
F
Forall [constructor, in Part1A]
Free [constructor, in Part1A]
H
head_inDom [lemma, in Binding]
I
II_Head [constructor, in Binding]
II_Skip [constructor, in Binding]
inContext [inductive, in Binding]
inContext_Bind [lemma, in Binding]
inContext_Bind_neg [lemma, in Binding]
inContext_contra [lemma, in Binding]
inContext_inDom [lemma, in Binding]
inDom [definition, in Binding]
inDom_Bind [lemma, in Binding]
insertInto [inductive, in Binding]
insertInto_inContext [lemma, in Binding]
insertInto_inContext' [lemma, in Binding]
insertInto_inContext2 [lemma, in Binding]
insertInto_inDom [lemma, in Binding]
insertInto_wfContext [lemma, in Binding]
insertInto_wfTy [lemma, in Binding]
In_Eq [constructor, in Binding]
In_Neq [constructor, in Binding]
M
move_wfContext [lemma, in Binding]
multiSwap [lemma, in Binding]
multiSwap' [lemma, in Binding]
N
narrowing [lemma, in Part1A]
narrowing' [lemma, in Part1A]
narrowing_eq [lemma, in Binding]
narrowing_inDom [lemma, in Binding]
narrowing_neq [lemma, in Binding]
narrowing_weakening [lemma, in Part1A]
narrowing_wfContext [lemma, in Binding]
narrowing_wfTerm [lemma, in Part1A]
narrowing_wfTerm [lemma, in Binding]
notBound_weaken [lemma, in Binding]
P
Part1A [library]
permutation [lemma, in Part1A]
permute [inductive, in Binding]
permute_inContext [lemma, in Binding]
permute_inContext' [lemma, in Binding]
permute_inDom [lemma, in Binding]
permute_inDom' [lemma, in Binding]
permute_inDom_neg [lemma, in Binding]
permute_refl [lemma, in Binding]
permute_wfContext [lemma, in Binding]
permute_wfTy [lemma, in Binding]
permute_wfTy [lemma, in Part1A]
PM_Bind [constructor, in Binding]
PM_Empty [constructor, in Binding]
preweaken_wfTy [lemma, in Part1A]
proj1_wfTy [lemma, in Part1A]
proj2_wfTy [lemma, in Part1A]
R
reflexivity [lemma, in Part1A]
S
SA_All [constructor, in Part1A]
SA_Arrow [constructor, in Part1A]
SA_Refl_TVar [constructor, in Part1A]
SA_Top [constructor, in Part1A]
SA_Trans_TVar [constructor, in Part1A]
split_inDom [lemma, in Binding]
squeeze_inContext [lemma, in Binding]
squeeze_inDom [lemma, in Binding]
subst [definition, in Part1A]
subTy [inductive, in Part1A]
subTy_wfContext [lemma, in Part1A]
subTy_wfTy [lemma, in Part1A]
subTy_wfTy1 [lemma, in Part1A]
subTy_wfTy2 [lemma, in Part1A]
switchBase_inDom [lemma, in Binding]
switchTerm_inDom [lemma, in Binding]
switchWeaken_inDom [lemma, in Binding]
switchWeaken_inDom' [lemma, in Binding]
T
Top [constructor, in Part1A]
Top_sub [lemma, in Part1A]
Top_sub' [lemma, in Part1A]
transitivity [lemma, in Part1A]
transitivity_and_narrowing [lemma, in Part1A]
ty [inductive, in Part1A]
tySize [definition, in Part1A]
tySize_subst [lemma, in Part1A]
ty_ind_syntactic [lemma, in Part1A]
U
use_narrowing [lemma, in Part1A]
V
var [definition, in Binding]
var_eq_dec [definition, in Binding]
W
weaken [definition, in Binding]
weakening [lemma, in Part1A]
weakening1 [lemma, in Part1A]
weaken_bind_assoc [lemma, in Binding]
weaken_inContext [lemma, in Binding]
weaken_inContext2 [lemma, in Binding]
weaken_inContext3 [lemma, in Binding]
weaken_inContext4 [lemma, in Binding]
weaken_inDom [lemma, in Binding]
weaken_inDom2 [lemma, in Binding]
weaken_inDom3 [lemma, in Binding]
weaken_inDom4 [lemma, in Binding]
weaken_wfTy [lemma, in Binding]
wfContext [inductive, in Binding]
wfContext_invert1 [lemma, in Binding]
wfContext_invert_weaken [lemma, in Binding]
wfTy [inductive, in Part1A]
WF_Arrow [constructor, in Part1A]
WF_Bind [constructor, in Binding]
WF_Empty [constructor, in Binding]
WF_Forall [constructor, in Part1A]
WF_Free [constructor, in Part1A]
WF_Top [constructor, in Part1A]
Lemma Index
C
cons_inDom [in Binding]
H
head_inDom [in Binding]
I
inContext_Bind [in Binding]
inContext_Bind_neg [in Binding]
inContext_contra [in Binding]
inContext_inDom [in Binding]
inDom_Bind [in Binding]
insertInto_inContext [in Binding]
insertInto_inContext' [in Binding]
insertInto_inContext2 [in Binding]
insertInto_inDom [in Binding]
insertInto_wfContext [in Binding]
insertInto_wfTy [in Binding]
M
move_wfContext [in Binding]
multiSwap [in Binding]
multiSwap' [in Binding]
N
narrowing [in Part1A]
narrowing' [in Part1A]
narrowing_eq [in Binding]
narrowing_inDom [in Binding]
narrowing_neq [in Binding]
narrowing_weakening [in Part1A]
narrowing_wfContext [in Binding]
narrowing_wfTerm [in Part1A]
narrowing_wfTerm [in Binding]
notBound_weaken [in Binding]
P
permutation [in Part1A]
permute_inContext [in Binding]
permute_inContext' [in Binding]
permute_inDom [in Binding]
permute_inDom' [in Binding]
permute_inDom_neg [in Binding]
permute_refl [in Binding]
permute_wfContext [in Binding]
permute_wfTy [in Binding]
permute_wfTy [in Part1A]
preweaken_wfTy [in Part1A]
proj1_wfTy [in Part1A]
proj2_wfTy [in Part1A]
R
reflexivity [in Part1A]
S
split_inDom [in Binding]
squeeze_inContext [in Binding]
squeeze_inDom [in Binding]
subTy_wfContext [in Part1A]
subTy_wfTy [in Part1A]
subTy_wfTy1 [in Part1A]
subTy_wfTy2 [in Part1A]
switchBase_inDom [in Binding]
switchTerm_inDom [in Binding]
switchWeaken_inDom [in Binding]
switchWeaken_inDom' [in Binding]
T
Top_sub [in Part1A]
Top_sub' [in Part1A]
transitivity [in Part1A]
transitivity_and_narrowing [in Part1A]
tySize_subst [in Part1A]
ty_ind_syntactic [in Part1A]
U
use_narrowing [in Part1A]
W
weakening [in Part1A]
weakening1 [in Part1A]
weaken_bind_assoc [in Binding]
weaken_inContext [in Binding]
weaken_inContext2 [in Binding]
weaken_inContext3 [in Binding]
weaken_inContext4 [in Binding]
weaken_inDom [in Binding]
weaken_inDom2 [in Binding]
weaken_inDom3 [in Binding]
weaken_inDom4 [in Binding]
weaken_wfTy [in Binding]
wfContext_invert1 [in Binding]
wfContext_invert_weaken [in Binding]
Constructor Index
A
Arrow [in Part1A]
B
Bind [in Binding]
Bound [in Part1A]
E
Empty [in Binding]
F
Forall [in Part1A]
Free [in Part1A]
I
II_Head [in Binding]
II_Skip [in Binding]
In_Eq [in Binding]
In_Neq [in Binding]
P
PM_Bind [in Binding]
PM_Empty [in Binding]
S
SA_All [in Part1A]
SA_Arrow [in Part1A]
SA_Refl_TVar [in Part1A]
SA_Top [in Part1A]
SA_Trans_TVar [in Part1A]
T
Top [in Part1A]
W
WF_Arrow [in Part1A]
WF_Bind [in Binding]
WF_Empty [in Binding]
WF_Forall [in Part1A]
WF_Free [in Part1A]
WF_Top [in Part1A]
Inductive Index
C
context [in Binding]
I
inContext [in Binding]
insertInto [in Binding]
P
permute [in Binding]
S
subTy [in Part1A]
T
ty [in Part1A]
W
wfContext [in Binding]
wfTy [in Part1A]
Definition Index
C
context [in Part1A]
I
inDom [in Binding]
S
subst [in Part1A]
T
tySize [in Part1A]
V
var [in Binding]
var_eq_dec [in Binding]
W
weaken [in Binding]
Library Index
B
Binding
P
Part1A
| 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 |
_ |
(113 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 |
_ |
(72 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 |
_ |
(24 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 |
_ |
(8 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 |
_ |
(7 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 |
_ |
(2 entries) |
This page has been generated by coqdoc