Global Index

G

H

K

Q

W

X

Y

Z

_

(236 entries)

Instance Index

A

B

C

D

E

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(1 entry)

Lemma Index

D

G

H

J

K

L

Q

R

W

X

Y

Z

_

other

(135 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

_

(20 entries)

Constructor Index

A

C

E

F

G

H

I

J

K

M

Q

S

U

V

W

X

Y

Z

_

other

(33 entries)

Inductive Index

A

D

E

F

G

H

I

K

O

Q

R

U

V

W

X

Y

Z

_

other

(9 entries)

Definition Index

A

D

E

G

H

I

K

M

Q

R

T

U

W

X

Y

Z

_

other

(20 entries)

Module Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

W

X

Y

Z

_

other

(5 entries)

Library Index

A

B

C

D

E

F

G

H

I

J

K

N

O

P

Q

S

T

U

V

W

X

Y

Z

_

other

(13 entries)

Global Index

A

arith_split [lemma, in LambdaJ_ndr]

B

beta_app_left [constructor, in Rewriting_defs]
beta_app_right [constructor, in Rewriting_defs]
beta_subst_right [constructor, in Rewriting_defs]
beta_subst_left [constructor, in Rewriting_defs]
beta_abs [constructor, in Rewriting_defs]
body [definition, in LambdaES_Infrastructure]
body_to_subs [lemma, in LambdaES_Infrastructure]
body_to_term_abs [lemma, in LambdaES_Infrastructure]
body_distribute_over_application [lemma, in LambdaES_Infrastructure]
body_abs [lemma, in LambdaES_Infrastructure]
body_open_term [lemma, in LambdaES_Infrastructure]
bv_occ_k_term [lemma, in LambdaES_occ]
bv_occ_body_term [lemma, in LambdaES_occ]
bv_occ_open_decompose_simpl [lemma, in LambdaES_occ]
bv_occ [definition, in LambdaES_occ]
bv_occ_open_decompose [lemma, in LambdaES_occ]
bv_occ_subst [lemma, in LambdaES_occ]
bv_occ_open_gen [lemma, in LambdaES_occ]
bv_occ_close_decompose [lemma, in LambdaES_occ]
bv_occ_term [lemma, in LambdaES_occ]
bv_occ_k [definition, in LambdaES_occ]
bv_occ_close_decompose_simpl [lemma, in LambdaES_occ]
B_red [inductive, in LambdaJ_Rules]
B_ctxt_red [definition, in LambdaJ_Rules]

C

close [definition, in LambdaES_Defs]
close_var_rec_open [lemma, in LambdaES_Infrastructure]
close_rec [definition, in LambdaES_Defs]
close_fresh [lemma, in LambdaES_Infrastructure]
close_var_body [lemma, in LambdaES_Infrastructure]
contextual_closure [inductive, in Rewriting_defs]

D

direct_reduction [constructor, in Rewriting_defs]

E

eq_var_dec [lemma, in Metatheory_Var]

F

finite_nat_list_max [lemma, in Metatheory_Var]
finite_nat_list_max' [lemma, in Metatheory_Var]
fresh [definition, in Metatheory_Var]
fresh_resize_length [lemma, in Metatheory_Fresh]
fresh_union_r2 [lemma, in Metatheory_Fresh]
fresh_union_r [lemma, in Metatheory_Fresh]
fresh_length [lemma, in Metatheory_Var]
fresh_morphism [instance, in Metatheory_Fresh]
fresh_resize [lemma, in Metatheory_Fresh]
fresh_union_r1 [lemma, in Metatheory_Fresh]
fresh_empty [lemma, in Metatheory_Fresh]
fresh_morphism_ [lemma, in Metatheory_Fresh]
fresh_union_l [lemma, in Metatheory_Fresh]
fresh_length [lemma, in Metatheory_Fresh]
fset_union_notin [lemma, in Metatheory_Var]
full_composition [lemma, in LambdaJ_Properties]
fv [definition, in LambdaES_Defs]
fvar_body [lemma, in LambdaES_Infrastructure]
fv_open_both_subset_notin [lemma, in LambdaES_fv]
fv_open [lemma, in LambdaES_occ]
fv_in_or_notin [lemma, in LambdaES_fv]
fv_open_both_notin_open [lemma, in LambdaES_fv]
fv_close [lemma, in LambdaES_fv]
fv_notin_open [lemma, in LambdaES_fv]
fv_in_open [lemma, in LambdaES_fv]
fv_occ_open [lemma, in LambdaES_occ]
fv_open_in [lemma, in LambdaES_fv]
fv_occ_close [lemma, in LambdaES_occ]
fv_occ_notin [lemma, in LambdaES_occ]
fv_open_both_subset_context_notin [lemma, in LambdaES_fv]
fv_open_notin [lemma, in LambdaES_fv]
fv_subst_commute [lemma, in LambdaJ_ndr]
fv_open_in_neq [lemma, in LambdaES_fv]
fv_open_ [lemma, in LambdaES_fv]
fv_occ_subs_decompose [lemma, in LambdaES_occ]
fv_occ_open_var [lemma, in LambdaES_occ]
fv_occ [definition, in LambdaES_occ]
fv_open_subset [lemma, in LambdaES_fv]
fv_open_both_notin [lemma, in LambdaES_fv]

I

in_singleton [lemma, in Metatheory_Var]
in_union [lemma, in Metatheory_Var]
in_empty [lemma, in Metatheory_Var]

J

j_ctxt_red [definition, in LambdaJ_Rules]
j_full_reduction [definition, in LambdaJ_Rules]
j_red [inductive, in LambdaJ_Rules]

L

LambdaES_occ [library]
LambdaES_Defs [library]
LambdaES_Infrastructure [library]
LambdaES_Tactics [library]
LambdaES_fv [library]
LambdaJ_Rules [library]
LambdaJ_Properties [library]
LambdaJ_ndr [library]
left_equation [constructor, in Rewriting_defs]
list_forall [inductive, in Metatheory_Tactics]
list_forall_cons [constructor, in Metatheory_Tactics]
list_for_n [definition, in Metatheory_Tactics]
list_forall_nil [constructor, in Metatheory_Tactics]

M

max_lt_l [lemma, in Metatheory_Var]
Metatheory [library]
Metatheory_Var [library]
Metatheory_Tactics [library]
Metatheory_Fresh [library]
modulo_reduction [inductive, in Rewriting_defs]

N

nat_ind_lambda_j [lemma, in LambdaJ_Rules]
ndr [definition, in LambdaJ_ndr]
ndr_n_fv_occ [lemma, in LambdaJ_ndr]
ndr_subst [lemma, in LambdaJ_ndr]
ndr_n_gt_fv [lemma, in LambdaJ_ndr]
ndr_abs [constructor, in LambdaJ_ndr]
ndr_n_fv_occ_x [lemma, in LambdaJ_ndr]
ndr_sub [constructor, in LambdaJ_ndr]
ndr_n [inductive, in LambdaJ_ndr]
ndr_n_opens_gen [lemma, in LambdaJ_ndr]
ndr_n_close_open [lemma, in LambdaJ_ndr]
ndr_n_exists [lemma, in LambdaJ_ndr]
ndr_n_preservation_term [lemma, in LambdaJ_ndr]
ndr_varnone [constructor, in LambdaJ_ndr]
ndr_bvar [constructor, in LambdaJ_ndr]
ndr_n_refl [lemma, in LambdaJ_ndr]
ndr_preservation_term [lemma, in LambdaJ_ndr]
ndr_n_opens [lemma, in LambdaJ_ndr]
ndr_exists [lemma, in LambdaJ_ndr]
ndr_varsome [constructor, in LambdaJ_ndr]
ndr_app [constructor, in LambdaJ_ndr]
ndr_n_occ_preservation [lemma, in LambdaJ_ndr]
ndr_n_preservation_body [lemma, in LambdaJ_ndr]
notin_singleton_l [lemma, in Metatheory_Var]
notin_fv_close [lemma, in LambdaES_fv]
notin_singleton_r [lemma, in Metatheory_Var]
notin_union_r [lemma, in Metatheory_Var]
notin_union_r1 [lemma, in Metatheory_Var]
notin_union [lemma, in Metatheory_Var]
notin_union_l [lemma, in Metatheory_Var]
notin_same [lemma, in Metatheory_Var]
notin_var_gen [lemma, in Metatheory_Var]
notin_union_r2 [lemma, in Metatheory_Var]
notin_var_gen [lemma, in Metatheory_Fresh]
notin_empty [lemma, in Metatheory_Var]
notin_singleton_swap [lemma, in Metatheory_Var]
notin_singleton [lemma, in Metatheory_Var]

O

one_step_reduction [constructor, in Rewriting_defs]
open [definition, in LambdaES_Defs]
open_close_var [lemma, in LambdaES_Infrastructure]
open_var_inj [lemma, in LambdaES_Infrastructure]
open_rec [definition, in LambdaES_Defs]
open_rec_term [lemma, in LambdaES_Infrastructure]
open_rec_term_core [lemma, in LambdaES_Infrastructure]

P

peano_induction [lemma, in LambdaES_Infrastructure]
preservation_terms_after_j [lemma, in LambdaJ_Rules]
preservation_terms_after_B [lemma, in LambdaJ_Rules]
pterm [inductive, in LambdaES_Defs]
pterm_size [definition, in LambdaES_Infrastructure]
pterm_sub [constructor, in LambdaES_Defs]
pterm_abs [constructor, in LambdaES_Defs]
pterm_bvar [constructor, in LambdaES_Defs]
pterm_fvar [constructor, in LambdaES_Defs]
pterm_app [constructor, in LambdaES_Defs]
pterm_size_open_var [lemma, in LambdaES_Infrastructure]

R

redex [constructor, in Rewriting_defs]
reflexive_reduction [constructor, in Rewriting_defs]
Rewriting_defs [library]
right_equation [constructor, in Rewriting_defs]
rule_d [constructor, in LambdaJ_Rules]
rule_c [constructor, in LambdaJ_Rules]
rule_B [constructor, in LambdaJ_Rules]
rule_w [constructor, in LambdaJ_Rules]

S

star_closure [inductive, in Rewriting_defs]
subset_empty_l [lemma, in Metatheory_Var]
subset_union_trans_l [lemma, in Metatheory_Var]
subset_union_var [lemma, in Metatheory_Var]
subset_union_l [lemma, in Metatheory_Var]
subset_union_weak_l [lemma, in Metatheory_Var]
subset_refl [lemma, in Metatheory_Var]
subset_singleton [lemma, in Metatheory_Var]
subset_union_weak_r [lemma, in Metatheory_Var]
subset_trans [lemma, in Metatheory_Var]
subset_union_trans_r [lemma, in Metatheory_Var]
subst [definition, in LambdaES_Infrastructure]
subst_open_var [lemma, in LambdaES_Infrastructure]
subst_intro [lemma, in LambdaES_Infrastructure]
subst_term [lemma, in LambdaES_Infrastructure]
subst_fresh [lemma, in LambdaES_Infrastructure]
subst_open [lemma, in LambdaES_Infrastructure]
subst_close [lemma, in LambdaES_Infrastructure]
subst_as_close_open [lemma, in LambdaES_Infrastructure]
subst_fv_occ [lemma, in LambdaES_occ]
subst_open_gen [lemma, in LambdaES_Infrastructure]

T

term [inductive, in LambdaES_Defs]
term_app_to_term_l [lemma, in LambdaES_Infrastructure]
term_app_to_term_r [lemma, in LambdaES_Infrastructure]
term_sub [constructor, in LambdaES_Defs]
term_open_term [lemma, in LambdaES_Infrastructure]
term_var [constructor, in LambdaES_Defs]
term_sub_to_body [lemma, in LambdaES_Infrastructure]
term_abs_to_body [lemma, in LambdaES_Infrastructure]
term_is_a_body [lemma, in LambdaES_Infrastructure]
term_size_induction [lemma, in LambdaES_Infrastructure]
term_app [constructor, in LambdaES_Defs]
term_to_subs [lemma, in LambdaES_Infrastructure]
term_abs_term [lemma, in LambdaES_Infrastructure]
term_sub_to_term [lemma, in LambdaES_Infrastructure]
term_abs [constructor, in LambdaES_Defs]
transitive_reduction [constructor, in Rewriting_defs]
transitive_closure_composition [lemma, in Rewriting_defs]

U

union_empty_r [lemma, in Metatheory_Var]
union_comm [lemma, in Metatheory_Var]
union_same [lemma, in Metatheory_Var]
union_assoc [lemma, in Metatheory_Var]
union_empty_l [lemma, in Metatheory_Var]
union_eq [lemma, in Metatheory_Var]
union_comm_assoc [lemma, in Metatheory_Var]

V

var [definition, in Metatheory_Var]
vars [definition, in Metatheory_Var]
VarSet [module, in Metatheory_Var]
var_fresh [lemma, in Metatheory_Var]
Var_as_OT [module, in Metatheory_Var]
var_freshes [lemma, in Metatheory_Var]
var_gen [definition, in Metatheory_Var]
var_gen_spec [lemma, in Metatheory_Var]
VSD [module, in Metatheory_Var]
VSF [module, in Metatheory_Var]
VSP [module, in Metatheory_Var]

other

_ -->B _ [notation, in LambdaJ_Rules]
_ === _ [notation, in Metatheory_Tactics]
_ [ _ ] [notation, in LambdaES_Defs]
_ [=] _ [notation, in Metatheory_Var]
_ \notin _ [notation, in Metatheory_Var]
_ \in _ [notation, in Metatheory_Var]
_ ^^ _ [notation, in LambdaES_Defs]
_ -->j* _ [notation, in LambdaJ_Rules]
_ -->j _ [notation, in LambdaJ_Rules]
_ << _ [notation, in Metatheory_Var]
_ \u _ [notation, in Metatheory_Var]
_ \rem _ [notation, in Metatheory_Var]
_ ->B _ [notation, in LambdaJ_Rules]
_ ^ _ [notation, in LambdaES_Defs]
_ == _ [notation, in Metatheory_Tactics]
_ ->j _ [notation, in LambdaJ_Rules]
[ _ ~> _ ] _ [notation, in LambdaES_Infrastructure]
{ _ ~> _ } _ [notation, in LambdaES_Defs]
{{ _ }} [notation, in Metatheory_Var]
{} [notation, in Metatheory_Var]

Instance Index

F

fresh_morphism [in Metatheory_Fresh]

Lemma Index

A

arith_split [in LambdaJ_ndr]

B

body_to_subs [in LambdaES_Infrastructure]
body_to_term_abs [in LambdaES_Infrastructure]
body_distribute_over_application [in LambdaES_Infrastructure]
body_abs [in LambdaES_Infrastructure]
body_open_term [in LambdaES_Infrastructure]
bv_occ_k_term [in LambdaES_occ]
bv_occ_body_term [in LambdaES_occ]
bv_occ_open_decompose_simpl [in LambdaES_occ]
bv_occ_open_decompose [in LambdaES_occ]
bv_occ_subst [in LambdaES_occ]
bv_occ_open_gen [in LambdaES_occ]
bv_occ_close_decompose [in LambdaES_occ]
bv_occ_term [in LambdaES_occ]
bv_occ_close_decompose_simpl [in LambdaES_occ]

C

close_var_rec_open [in LambdaES_Infrastructure]
close_fresh [in LambdaES_Infrastructure]
close_var_body [in LambdaES_Infrastructure]

E

eq_var_dec [in Metatheory_Var]

F

finite_nat_list_max [in Metatheory_Var]
finite_nat_list_max' [in Metatheory_Var]
fresh_resize_length [in Metatheory_Fresh]
fresh_union_r2 [in Metatheory_Fresh]
fresh_union_r [in Metatheory_Fresh]
fresh_length [in Metatheory_Var]
fresh_resize [in Metatheory_Fresh]
fresh_union_r1 [in Metatheory_Fresh]
fresh_empty [in Metatheory_Fresh]
fresh_morphism_ [in Metatheory_Fresh]
fresh_union_l [in Metatheory_Fresh]
fresh_length [in Metatheory_Fresh]
fset_union_notin [in Metatheory_Var]
full_composition [in LambdaJ_Properties]
fvar_body [in LambdaES_Infrastructure]
fv_open_both_subset_notin [in LambdaES_fv]
fv_open [in LambdaES_occ]
fv_in_or_notin [in LambdaES_fv]
fv_open_both_notin_open [in LambdaES_fv]
fv_close [in LambdaES_fv]
fv_notin_open [in LambdaES_fv]
fv_in_open [in LambdaES_fv]
fv_occ_open [in LambdaES_occ]
fv_open_in [in LambdaES_fv]
fv_occ_close [in LambdaES_occ]
fv_occ_notin [in LambdaES_occ]
fv_open_both_subset_context_notin [in LambdaES_fv]
fv_open_notin [in LambdaES_fv]
fv_subst_commute [in LambdaJ_ndr]
fv_open_in_neq [in LambdaES_fv]
fv_open_ [in LambdaES_fv]
fv_occ_subs_decompose [in LambdaES_occ]
fv_occ_open_var [in LambdaES_occ]
fv_open_subset [in LambdaES_fv]
fv_open_both_notin [in LambdaES_fv]

I

in_singleton [in Metatheory_Var]
in_union [in Metatheory_Var]
in_empty [in Metatheory_Var]

M

max_lt_l [in Metatheory_Var]

N

nat_ind_lambda_j [in LambdaJ_Rules]
ndr_n_fv_occ [in LambdaJ_ndr]
ndr_subst [in LambdaJ_ndr]
ndr_n_gt_fv [in LambdaJ_ndr]
ndr_n_fv_occ_x [in LambdaJ_ndr]
ndr_n_opens_gen [in LambdaJ_ndr]
ndr_n_close_open [in LambdaJ_ndr]
ndr_n_exists [in LambdaJ_ndr]
ndr_n_preservation_term [in LambdaJ_ndr]
ndr_n_refl [in LambdaJ_ndr]
ndr_preservation_term [in LambdaJ_ndr]
ndr_n_opens [in LambdaJ_ndr]
ndr_exists [in LambdaJ_ndr]
ndr_n_occ_preservation [in LambdaJ_ndr]
ndr_n_preservation_body [in LambdaJ_ndr]
notin_singleton_l [in Metatheory_Var]
notin_fv_close [in LambdaES_fv]
notin_singleton_r [in Metatheory_Var]
notin_union_r [in Metatheory_Var]
notin_union_r1 [in Metatheory_Var]
notin_union [in Metatheory_Var]
notin_union_l [in Metatheory_Var]
notin_same [in Metatheory_Var]
notin_var_gen [in Metatheory_Var]
notin_union_r2 [in Metatheory_Var]
notin_var_gen [in Metatheory_Fresh]
notin_empty [in Metatheory_Var]
notin_singleton_swap [in Metatheory_Var]
notin_singleton [in Metatheory_Var]

O

open_close_var [in LambdaES_Infrastructure]
open_var_inj [in LambdaES_Infrastructure]
open_rec_term [in LambdaES_Infrastructure]
open_rec_term_core [in LambdaES_Infrastructure]

P

peano_induction [in LambdaES_Infrastructure]
preservation_terms_after_j [in LambdaJ_Rules]
preservation_terms_after_B [in LambdaJ_Rules]
pterm_size_open_var [in LambdaES_Infrastructure]

S

subset_empty_l [in Metatheory_Var]
subset_union_trans_l [in Metatheory_Var]
subset_union_var [in Metatheory_Var]
subset_union_l [in Metatheory_Var]
subset_union_weak_l [in Metatheory_Var]
subset_refl [in Metatheory_Var]
subset_singleton [in Metatheory_Var]
subset_union_weak_r [in Metatheory_Var]
subset_trans [in Metatheory_Var]
subset_union_trans_r [in Metatheory_Var]
subst_open_var [in LambdaES_Infrastructure]
subst_intro [in LambdaES_Infrastructure]
subst_term [in LambdaES_Infrastructure]
subst_fresh [in LambdaES_Infrastructure]
subst_open [in LambdaES_Infrastructure]
subst_close [in LambdaES_Infrastructure]
subst_as_close_open [in LambdaES_Infrastructure]
subst_fv_occ [in LambdaES_occ]
subst_open_gen [in LambdaES_Infrastructure]

T

term_app_to_term_l [in LambdaES_Infrastructure]
term_app_to_term_r [in LambdaES_Infrastructure]
term_open_term [in LambdaES_Infrastructure]
term_sub_to_body [in LambdaES_Infrastructure]
term_abs_to_body [in LambdaES_Infrastructure]
term_is_a_body [in LambdaES_Infrastructure]
term_size_induction [in LambdaES_Infrastructure]
term_to_subs [in LambdaES_Infrastructure]
term_abs_term [in LambdaES_Infrastructure]
term_sub_to_term [in LambdaES_Infrastructure]
transitive_closure_composition [in Rewriting_defs]

U

union_empty_r [in Metatheory_Var]
union_comm [in Metatheory_Var]
union_same [in Metatheory_Var]
union_assoc [in Metatheory_Var]
union_empty_l [in Metatheory_Var]
union_eq [in Metatheory_Var]
union_comm_assoc [in Metatheory_Var]

V

var_fresh [in Metatheory_Var]
var_freshes [in Metatheory_Var]
var_gen_spec [in Metatheory_Var]

Notation Index

other

_ -->B _ [in LambdaJ_Rules]
_ === _ [in Metatheory_Tactics]
_ [ _ ] [in LambdaES_Defs]
_ [=] _ [in Metatheory_Var]
_ \notin _ [in Metatheory_Var]
_ \in _ [in Metatheory_Var]
_ ^^ _ [in LambdaES_Defs]
_ -->j* _ [in LambdaJ_Rules]
_ -->j _ [in LambdaJ_Rules]
_ << _ [in Metatheory_Var]
_ \u _ [in Metatheory_Var]
_ \rem _ [in Metatheory_Var]
_ ->B _ [in LambdaJ_Rules]
_ ^ _ [in LambdaES_Defs]
_ == _ [in Metatheory_Tactics]
_ ->j _ [in LambdaJ_Rules]
[ _ ~> _ ] _ [in LambdaES_Infrastructure]
{ _ ~> _ } _ [in LambdaES_Defs]
{{ _ }} [in Metatheory_Var]
{} [in Metatheory_Var]

Constructor Index

B

beta_app_left [in Rewriting_defs]
beta_app_right [in Rewriting_defs]
beta_subst_right [in Rewriting_defs]
beta_subst_left [in Rewriting_defs]
beta_abs [in Rewriting_defs]

D

direct_reduction [in Rewriting_defs]

L

left_equation [in Rewriting_defs]
list_forall_cons [in Metatheory_Tactics]
list_forall_nil [in Metatheory_Tactics]

N

ndr_abs [in LambdaJ_ndr]
ndr_sub [in LambdaJ_ndr]
ndr_varnone [in LambdaJ_ndr]
ndr_bvar [in LambdaJ_ndr]
ndr_varsome [in LambdaJ_ndr]
ndr_app [in LambdaJ_ndr]

O

one_step_reduction [in Rewriting_defs]

P

pterm_sub [in LambdaES_Defs]
pterm_abs [in LambdaES_Defs]
pterm_bvar [in LambdaES_Defs]
pterm_fvar [in LambdaES_Defs]
pterm_app [in LambdaES_Defs]

R

redex [in Rewriting_defs]
reflexive_reduction [in Rewriting_defs]
right_equation [in Rewriting_defs]
rule_d [in LambdaJ_Rules]
rule_c [in LambdaJ_Rules]
rule_B [in LambdaJ_Rules]
rule_w [in LambdaJ_Rules]

T

term_sub [in LambdaES_Defs]
term_var [in LambdaES_Defs]
term_app [in LambdaES_Defs]
term_abs [in LambdaES_Defs]
transitive_reduction [in Rewriting_defs]

Inductive Index

B

B_red [in LambdaJ_Rules]

C

contextual_closure [in Rewriting_defs]

J

j_red [in LambdaJ_Rules]

L

list_forall [in Metatheory_Tactics]

M

modulo_reduction [in Rewriting_defs]

N

ndr_n [in LambdaJ_ndr]

P

pterm [in LambdaES_Defs]

S

star_closure [in Rewriting_defs]

T

term [in LambdaES_Defs]

Definition Index

B

body [in LambdaES_Infrastructure]
bv_occ [in LambdaES_occ]
bv_occ_k [in LambdaES_occ]
B_ctxt_red [in LambdaJ_Rules]

C

close [in LambdaES_Defs]
close_rec [in LambdaES_Defs]

F

fresh [in Metatheory_Var]
fv [in LambdaES_Defs]
fv_occ [in LambdaES_occ]

J

j_ctxt_red [in LambdaJ_Rules]
j_full_reduction [in LambdaJ_Rules]

L

list_for_n [in Metatheory_Tactics]

N

ndr [in LambdaJ_ndr]

O

open [in LambdaES_Defs]
open_rec [in LambdaES_Defs]

P

pterm_size [in LambdaES_Infrastructure]

S

subst [in LambdaES_Infrastructure]

V

var [in Metatheory_Var]
vars [in Metatheory_Var]
var_gen [in Metatheory_Var]

Module Index

V

VarSet [in Metatheory_Var]
Var_as_OT [in Metatheory_Var]
VSD [in Metatheory_Var]
VSF [in Metatheory_Var]
VSP [in Metatheory_Var]

Library Index

L

LambdaES_occ
LambdaES_Defs
LambdaES_Infrastructure
LambdaES_Tactics
LambdaES_fv
LambdaJ_Rules
LambdaJ_Properties
LambdaJ_ndr

M

Metatheory
Metatheory_Var
Metatheory_Tactics
Metatheory_Fresh

R

Global Index

G

H

K

Q

W

X

Y

Z

_

(236 entries)

Instance Index

A

B

C

D

E

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(1 entry)

Lemma Index

D

G

H

J

K

L

Q

R

W

X

Y

Z

_

other

(135 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

_

(20 entries)

Constructor Index

A

C

E

F

G

H

I

J

K

M

Q

S

U

V

W

X

Y

Z

_

other

(33 entries)

Inductive Index

A

D

E

F

G

H

I

K

O

Q

R

U

V

W

X

Y

Z

_

other

(9 entries)

Definition Index

A

D

E

G

H

I

K

M

Q

R

T

U

W

X

Y

Z

_

other

(20 entries)

Module Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

W

X

Y

Z

_

other

(5 entries)

Library Index

A

B

C

D

E

F

G

H

I

J

K

N

O

P

Q

S

T

U

V

W

X

Y

Z

_

other

(13 entries)

This page has been generated by coqdoc