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

_

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

_

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

_

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

_

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

_

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

_

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

_

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

_

(96 entries)

---

S

Sbtrm_bind [constructor, in Lambda.Terms]
Sbtrm_bind [constructor, in Lambda.TPOSR.Terms]
Sbtrm_nobind [constructor, in Lambda.Terms]
Sbtrm_nobind [constructor, in Lambda.TPOSR.Terms]
set [constructor, in Lambda.Terms]
sigma_functionality [lemma, in Lambda.TPOSR.TypesFunctionality]
simpl_lift [lemma, in Lambda.LiftSubst]
simpl_lift_rec [lemma, in Lambda.LiftSubst]
simpl_llift [lemma, in Lambda.TPOSR.LiftSubst]
simpl_llift_rec [lemma, in Lambda.TPOSR.LiftSubst]
simpl_lsubst [lemma, in Lambda.TPOSR.LiftSubst]
simpl_lsubst_rec [lemma, in Lambda.TPOSR.LiftSubst]
simpl_subst [lemma, in Lambda.LiftSubst]
simpl_subst_rec [lemma, in Lambda.LiftSubst]
sn [definition, in Lambda.TPOSR.Reduction]
sn [definition, in Lambda.Reduction]
sn_lred_sn [lemma, in Lambda.TPOSR.Reduction]
sn_lsubst [lemma, in Lambda.TPOSR.Reduction]
sn_pair [lemma, in Lambda.Reduction]
sn_pair [lemma, in Lambda.TPOSR.Reduction]
sn_prod [lemma, in Lambda.Reduction]
sn_prod [lemma, in Lambda.TPOSR.Reduction]
sn_red_sn [lemma, in Lambda.Reduction]
sn_subset [lemma, in Lambda.Reduction]
sn_subset [lemma, in Lambda.TPOSR.Reduction]
sn_subst [lemma, in Lambda.Reduction]
sn_sum [lemma, in Lambda.Reduction]
sn_sum [lemma, in Lambda.TPOSR.Reduction]
sort [inductive, in Lambda.Terms]
sorting_lambda [lemma, in Lambda.Russell.Generation]
sorting_lambda_aux [lemma, in Lambda.Russell.Generation]
sorts_of_sorted [lemma, in Lambda.Russell.GenerationCoerce]
sorts_of_sorted [lemma, in Lambda.JRussell.GenerationCoerce]
sort_conv_eq [lemma, in Lambda.Russell.GenerationCoerce]
sort_conv_eq [lemma, in Lambda.JRussell.GenerationCoerce]
sort_eq_eq [lemma, in Lambda.JRussell.GenerationCoerce]
sort_judgement_empty_env [lemma, in Lambda.JRussell.Validity]
sort_level_ind [lemma, in Lambda.Terms]
sort_of_abs_range [lemma, in Lambda.Russell.GenerationRange]
sort_of_abs_range [lemma, in Lambda.JRussell.GenerationRange]
sort_of_abs_range_aux [lemma, in Lambda.JRussell.GenerationRange]
sort_of_abs_range_aux [lemma, in Lambda.Russell.GenerationRange]
sort_of_app [lemma, in Lambda.Russell.Generation]
sort_of_app2 [lemma, in Lambda.Russell.Generation]
sort_of_app_aux [lemma, in Lambda.Russell.Generation]
sort_of_app_aux2 [lemma, in Lambda.Russell.Generation]
sort_of_app_range [lemma, in Lambda.JRussell.GenerationRange]
sort_of_app_range [lemma, in Lambda.Russell.GenerationRange]
sort_of_app_range_aux [lemma, in Lambda.JRussell.GenerationRange]
sort_of_app_range_aux [lemma, in Lambda.Russell.GenerationRange]
sort_of_kinded [lemma, in Lambda.Russell.GenerationCoerce]
sort_of_kinded [lemma, in Lambda.JRussell.GenerationCoerce]
sort_of_kinded_aux [lemma, in Lambda.Russell.GenerationCoerce]
sort_of_kinded_aux [lemma, in Lambda.JRussell.GenerationCoerce]
sort_of_pair_range [lemma, in Lambda.JRussell.GenerationRange]
sort_of_pair_range [lemma, in Lambda.Russell.GenerationRange]
sort_of_pair_range_aux [lemma, in Lambda.Russell.GenerationRange]
sort_of_pair_range_aux [lemma, in Lambda.JRussell.GenerationRange]
sort_of_pi1_range [lemma, in Lambda.Russell.GenerationRange]
sort_of_pi1_range [lemma, in Lambda.JRussell.GenerationRange]
sort_of_pi1_range_aux [lemma, in Lambda.Russell.GenerationRange]
sort_of_pi1_range_aux [lemma, in Lambda.JRussell.GenerationRange]
sort_of_pi2_range [lemma, in Lambda.Russell.GenerationRange]
sort_of_pi2_range [lemma, in Lambda.JRussell.GenerationRange]
sort_of_pi2_range_aux [lemma, in Lambda.Russell.GenerationRange]
sort_of_pi2_range_aux [lemma, in Lambda.JRussell.GenerationRange]
sort_of_propset [lemma, in Lambda.JRussell.GenerationCoerce]
sort_of_propset [lemma, in Lambda.Russell.GenerationCoerce]
sort_of_sum [lemma, in Lambda.Russell.GenerationRange]
sort_of_sum [lemma, in Lambda.JRussell.GenerationRange]
sort_of_sum_aux [lemma, in Lambda.JRussell.GenerationRange]
sort_of_sum_aux [lemma, in Lambda.Russell.GenerationRange]
sort_par_lred [constructor, in Lambda.TPOSR.Reduction]
sort_par_red [constructor, in Lambda.Reduction]
Srt [constructor, in Lambda.Terms]
Srt_l [constructor, in Lambda.TPOSR.Terms]
strength_sort_judgement [lemma, in Lambda.JRussell.Validity]
strength_sort_judgement [lemma, in Lambda.Russell.Generation]
strip_lemma [lemma, in Lambda.TPOSR.Conv]
strip_lemma [lemma, in Lambda.Conv]
str_confluence_par_lred1 [lemma, in Lambda.TPOSR.Conv]
str_confluence_par_red1 [lemma, in Lambda.Conv]
str_confluent [definition, in Lambda.TPOSR.Conv]
str_confluent [definition, in Lambda.Conv]
SubjectReduction [library]
SubjectReduction [library]
SubjectReduction [library]
SubjectReduction [library]
subject_reduction [lemma, in Lambda.CCSum.SubjectReduction]
subject_reduction [lemma, in Lambda.Russell.SubjectReduction]
subject_reduction [lemma, in Lambda.TPOSR.SubjectReduction]
subject_reduction_depth [lemma, in Lambda.TPOSR.SubjectReduction]
subject_reduction_p [lemma, in Lambda.TPOSR.SubjectReduction]
subj_red [lemma, in Lambda.Russell.SubjectReduction]
subj_red [lemma, in Lambda.CCSum.SubjectReduction]
sublterm [inductive, in Lambda.TPOSR.Terms]
sublterm_abs [lemma, in Lambda.TPOSR.Reduction]
sublterm_ord_norm [lemma, in Lambda.TPOSR.Conv_Dec]
sublterm_prod [lemma, in Lambda.TPOSR.Reduction]
sublterm_sn [lemma, in Lambda.TPOSR.Reduction]
sublterm_subset [lemma, in Lambda.TPOSR.Reduction]
sublterm_sum [lemma, in Lambda.TPOSR.Reduction]
Subset [constructor, in Lambda.Terms]
subset_conv_left [lemma, in Lambda.TPOSR.TypesFunctionality]
subset_conv_right [lemma, in Lambda.TPOSR.TypesFunctionality]
subset_conv_right_aux [lemma, in Lambda.TPOSR.TypesFunctionality]
subset_functionality [lemma, in Lambda.TPOSR.TypesFunctionality]
subset_functionality_aux [lemma, in Lambda.TPOSR.TypesFunctionality]
Subset_l [constructor, in Lambda.TPOSR.Terms]
subset_lred_l [constructor, in Lambda.TPOSR.Reduction]
subset_lred_r [constructor, in Lambda.TPOSR.Reduction]
subset_par_lred [constructor, in Lambda.TPOSR.Reduction]
subset_par_red [constructor, in Lambda.Reduction]
subset_red_l [constructor, in Lambda.Reduction]
subset_red_r [constructor, in Lambda.Reduction]
subst [definition, in Lambda.Terms]
substitution [lemma, in Lambda.TPOSR.Substitution]
substitution [lemma, in Lambda.Russell.Substitution]
substitution [lemma, in Lambda.CCSum.Substitution]
substitution [lemma, in Lambda.JRussell.Substitution]
Substitution [library]
Substitution [library]
Substitution [library]
Substitution [library]
SubstitutionTPOSR [library]
substitution_coerce [lemma, in Lambda.JRussell.Substitution]
substitution_coerce [lemma, in Lambda.TPOSR.Substitution]
substitution_coerce [lemma, in Lambda.Russell.Substitution]
substitution_coerce_conv_l [lemma, in Lambda.Russell.Substitution]
substitution_coerce_conv_l_n [lemma, in Lambda.Russell.Substitution]
substitution_coerce_eq [lemma, in Lambda.TPOSR.UnlabConv]
substitution_coerce_n [lemma, in Lambda.TPOSR.Substitution]
substitution_coerce_tposrp [lemma, in Lambda.TPOSR.CtxCoercion]
substitution_eq [lemma, in Lambda.TPOSR.Substitution]
substitution_eq_n [lemma, in Lambda.TPOSR.Substitution]
substitution_jeq [lemma, in Lambda.JRussell.Substitution]
substitution_sorted [lemma, in Lambda.TPOSR.SubstitutionTPOSR]
substitution_sorted [lemma, in Lambda.TPOSR.Substitution]
substitution_sorted [lemma, in Lambda.TPOSR.PreSubstitutionTPOSR]
substitution_sorted_n [lemma, in Lambda.TPOSR.PreSubstitutionTPOSR]
substitution_sorted_n [lemma, in Lambda.TPOSR.Substitution]
substitution_sorted_n [lemma, in Lambda.TPOSR.SubstitutionTPOSR]
substitution_tposrp [lemma, in Lambda.TPOSR.Substitution]
substitution_tposrp_aux [lemma, in Lambda.TPOSR.Substitution]
substitution_tposrp_coerce [lemma, in Lambda.TPOSR.TPOSR_trans]
substitution_tposrp_tposr [lemma, in Lambda.TPOSR.TPOSR_trans]
substitution_tposr_coerce [lemma, in Lambda.TPOSR.SubstitutionTPOSR]
substitution_tposr_coerce [lemma, in Lambda.TPOSR.PreSubstitutionTPOSR]
substitution_tposr_coerce_n [lemma, in Lambda.TPOSR.PreSubstitutionTPOSR]
substitution_tposr_coerce_n [lemma, in Lambda.TPOSR.SubstitutionTPOSR]
substitution_tposr_eq [lemma, in Lambda.TPOSR.PreSubstitutionTPOSR]
substitution_tposr_eq [lemma, in Lambda.TPOSR.SubstitutionTPOSR]
substitution_tposr_eq_n [lemma, in Lambda.TPOSR.PreSubstitutionTPOSR]
substitution_tposr_eq_n [lemma, in Lambda.TPOSR.SubstitutionTPOSR]
substitution_tposr_n [lemma, in Lambda.TPOSR.Substitution]
substitution_tposr_tposr [lemma, in Lambda.TPOSR.PreSubstitutionTPOSR]
substitution_tposr_tposr [lemma, in Lambda.TPOSR.SubstitutionTPOSR]
substitution_tposr_tposrp [lemma, in Lambda.TPOSR.PreSubstitutionTPOSR]
substitution_tposr_tposrp [lemma, in Lambda.TPOSR.SubstitutionTPOSR]
substitution_tposr_tposrp_aux [lemma, in Lambda.TPOSR.SubstitutionTPOSR]
substitution_tposr_tposrp_aux [lemma, in Lambda.TPOSR.PreSubstitutionTPOSR]
substitution_tposr_tposr_n [lemma, in Lambda.TPOSR.PreSubstitutionTPOSR]
substitution_tposr_tposr_n [lemma, in Lambda.TPOSR.SubstitutionTPOSR]
substitution_tposr_tposr_wf_n [lemma, in Lambda.TPOSR.SubstitutionTPOSR]
substitution_tposr_tposr_wf_n [lemma, in Lambda.TPOSR.PreSubstitutionTPOSR]
substitution_tposr_wf_n [lemma, in Lambda.TPOSR.Substitution]
subst_rec [definition, in Lambda.Terms]
subst_ref_eq [lemma, in Lambda.LiftSubst]
subst_ref_gt [lemma, in Lambda.LiftSubst]
subst_ref_lt [lemma, in Lambda.LiftSubst]
subst_to_sort [lemma, in Lambda.JRussell.GenerationCoerce]
subst_to_sort [lemma, in Lambda.Russell.GenerationCoerce]
subterm [inductive, in Lambda.Terms]
subterm_abs [lemma, in Lambda.Reduction]
subterm_ord_norm [lemma, in Lambda.Conv_Dec]
subterm_prod [lemma, in Lambda.Reduction]
subterm_sn [lemma, in Lambda.Reduction]
subterm_subset [lemma, in Lambda.Reduction]
subterm_sum [lemma, in Lambda.Reduction]
subt_bind [inductive, in Lambda.TPOSR.Terms]
subt_bind [inductive, in Lambda.Terms]
subt_nobind [inductive, in Lambda.Terms]
subt_nobind [inductive, in Lambda.TPOSR.Terms]
sub_in_env [inductive, in Lambda.CCSum.Substitution]
sub_in_env [inductive, in Lambda.Env]
sub_in_lenv [inductive, in Lambda.TPOSR.Env]
sub_O [constructor, in Lambda.TPOSR.Env]
sub_O [constructor, in Lambda.Env]
sub_O [constructor, in Lambda.CCSum.Substitution]
sub_red_env [lemma, in Lambda.TPOSR.PreSubstitutionTPOSR]
sub_S [constructor, in Lambda.CCSum.Substitution]
sub_S [constructor, in Lambda.Env]
sub_S [constructor, in Lambda.TPOSR.Env]
Sum [constructor, in Lambda.Terms]
sum_conv_left [lemma, in Lambda.TPOSR.TypesFunctionality]
sum_conv_right [lemma, in Lambda.TPOSR.TypesFunctionality]
sum_conv_right_aux [lemma, in Lambda.TPOSR.TypesFunctionality]
Sum_l [constructor, in Lambda.TPOSR.Terms]
sum_lred_l [constructor, in Lambda.TPOSR.Reduction]
sum_lred_r [constructor, in Lambda.TPOSR.Reduction]
sum_par_lred [constructor, in Lambda.TPOSR.Reduction]
sum_par_red [constructor, in Lambda.Reduction]
sum_red_l [constructor, in Lambda.Reduction]
sum_red_r [constructor, in Lambda.Reduction]
sum_sort [definition, in Lambda.JRussell.Types]
sum_sort [definition, in Lambda.Russell.Types]
sum_sort [definition, in Lambda.TPOSR.Types]
sum_sort_functional [lemma, in Lambda.TPOSR.UniquenessOfTypes]
sum_sort_functional [lemma, in Lambda.JRussell.UnicityOfSortingRange]
sum_sort_prop [lemma, in Lambda.JRussell.GenerationRange]
sum_sort_prop [lemma, in Lambda.Russell.GenerationRange]
sym_conv [lemma, in Lambda.Reduction]
sym_conv [lemma, in Lambda.TPOSR.Reduction]

---

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

_

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

_

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

_

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

_

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

_

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

_

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

_

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

_

(96 entries)

---

Index

---

This page has been generated by coqdoc