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)

---

I (lemma)

incl_app_sym [in Lambda.MyList]
ind_coerce_env [in Lambda.JRussell.Coercion]
ind_conv_env [in Lambda.JRussell.Conversion]
ind_exp_env [in Lambda.TPOSR.CtxExpansion]
ind_left_refl [in Lambda.TPOSR.LeftReflexivity]
ind_pre_coerce_env [in Lambda.TPOSR.PreCtxCoercion]
ind_red_env [in Lambda.TPOSR.CtxReduction]
ind_right_refl [in Lambda.TPOSR.RightReflexivity]
ind_substitution [in Lambda.TPOSR.Substitution]
ind_substitution_tposr [in Lambda.TPOSR.PreSubstitutionTPOSR]
ind_sub_weak [in Lambda.JRussell.Substitution]
ind_thinning [in Lambda.TPOSR.Thinning]
ind_validity [in Lambda.TPOSR.Validity]
ind_weak_weak [in Lambda.JRussell.Thinning]
injectivity_of_pi [in Lambda.TPOSR.ChurchRosser]
injectivity_of_pi_coerce [in Lambda.TPOSR.Injectivity]
injectivity_of_pi_coerce_rc_depth_aux [in Lambda.TPOSR.Injectivity]
injectivity_of_subset [in Lambda.TPOSR.ChurchRosser]
injectivity_of_sum [in Lambda.TPOSR.ChurchRosser]
injectivity_of_sum_coerce [in Lambda.TPOSR.Injectivity]
injectivity_of_sum_coerce_rc_depth_aux [in Lambda.TPOSR.Injectivity]
ins_eq [in Lambda.MyList]
ins_gt [in Lambda.MyList]
ins_item_ge [in Lambda.TPOSR.Env]
ins_item_ge [in Lambda.Env]
ins_item_ge [in Lambda.CCSum.Thinning]
ins_item_lt [in Lambda.TPOSR.Env]
ins_item_lt [in Lambda.CCSum.Thinning]
ins_item_lt [in Lambda.Env]
ins_le [in Lambda.MyList]
inv_conv_prod_l [in Lambda.Conv]
inv_conv_prod_l [in Lambda.TPOSR.Conv]
inv_conv_prod_r [in Lambda.TPOSR.Conv]
inv_conv_prod_r [in Lambda.Conv]
inv_conv_prod_sort_l [in Lambda.Russell.Injectivity]
inv_conv_prod_sort_l_set [in Lambda.Russell.Injectivity]
inv_conv_prod_sort_r [in Lambda.Russell.Injectivity]
inv_conv_prod_sort_r_set [in Lambda.Russell.Injectivity]
inv_conv_subset_l [in Lambda.TPOSR.Conv]
inv_conv_subset_l [in Lambda.Conv]
inv_conv_subset_r [in Lambda.Conv]
inv_conv_subset_r [in Lambda.TPOSR.Conv]
inv_conv_sum_l [in Lambda.Conv]
inv_conv_sum_l [in Lambda.TPOSR.Conv]
inv_conv_sum_r [in Lambda.Conv]
inv_conv_sum_r [in Lambda.TPOSR.Conv]
inv_conv_sum_sort [in Lambda.Russell.Injectivity]
inv_conv_sum_sort_l_set [in Lambda.Russell.Injectivity]
inv_conv_sum_sort_r_set [in Lambda.Russell.Injectivity]
inv_eq_prod_l [in Lambda.TPOSR.CoerceNoTrans]
inv_eq_prod_r [in Lambda.TPOSR.CoerceNoTrans]
inv_eq_subset_l_set [in Lambda.TPOSR.CoerceNoTrans]
inv_eq_sum_l [in Lambda.TPOSR.CoerceNoTrans]
inv_eq_sum_r [in Lambda.TPOSR.CoerceNoTrans]
inv_lift_abs [in Lambda.InvLiftSubst]
inv_lift_app [in Lambda.InvLiftSubst]
inv_lift_pair [in Lambda.InvLiftSubst]
inv_lift_pi1 [in Lambda.InvLiftSubst]
inv_lift_pi2 [in Lambda.InvLiftSubst]
inv_lift_prod [in Lambda.InvLiftSubst]
inv_lift_ref [in Lambda.JRussell.Generation]
inv_lift_ref [in Lambda.TPOSR.Generation]
inv_lift_sort [in Lambda.Russell.Generation]
inv_lift_sort [in Lambda.InvLiftSubst]
inv_lift_subset [in Lambda.InvLiftSubst]
inv_lift_sum [in Lambda.InvLiftSubst]
inv_llift_sort [in Lambda.TPOSR.Equiv]
inv_nth_cs [in Lambda.MyList]
inv_nth_nl [in Lambda.MyList]
inv_par_lred_abs [in Lambda.TPOSR.Reduction]
inv_par_lred_pair [in Lambda.TPOSR.Reduction]
inv_par_red_abs [in Lambda.Reduction]
inv_par_red_pair [in Lambda.Reduction]
inv_subst_sort [in Lambda.Russell.Generation]
inv_subst_sort [in Lambda.InvLiftSubst]
inv_subst_sort [in Lambda.TPOSR.Equiv]
inv_sub_prod_l [in Lambda.Russell.SubjectReduction]
inv_sub_prod_l_aux [in Lambda.Russell.SubjectReduction]
inv_sub_prod_r [in Lambda.Russell.SubjectReduction]
inv_sub_sum_aux [in Lambda.Russell.SubjectReduction]
inv_sub_sum_l [in Lambda.Russell.SubjectReduction]
inv_sub_sum_r [in Lambda.Russell.SubjectReduction]
inv_type_coerce [in Lambda.Russell.Inversion]
inv_type_coerce [in Lambda.Russell.Inversion]
inv_type_conv [in Lambda.CCSum.Inversion]
inv_typ_abs [in Lambda.CCSum.Inversion]
inv_typ_abs [in Lambda.Russell.Inversion]
inv_typ_abs [in Lambda.Russell.Inversion]
inv_typ_abs2 [in Lambda.Russell.Inversion]
inv_typ_abs2 [in Lambda.Russell.Inversion]
inv_typ_app [in Lambda.CCSum.Inversion]
inv_typ_app [in Lambda.Russell.Inversion]
inv_typ_app [in Lambda.Russell.Inversion]
inv_typ_conv_kind [in Lambda.Russell.Inversion]
inv_typ_conv_kind [in Lambda.Russell.Inversion]
inv_typ_conv_kind [in Lambda.CCSum.Inversion]
inv_typ_kind [in Lambda.CCSum.Inversion]
inv_typ_pair [in Lambda.Russell.Inversion]
inv_typ_pair [in Lambda.Russell.Inversion]
inv_typ_pair [in Lambda.CCSum.Inversion]
inv_typ_pi1 [in Lambda.CCSum.Inversion]
inv_typ_pi1 [in Lambda.Russell.Inversion]
inv_typ_pi1 [in Lambda.Russell.Inversion]
inv_typ_pi2 [in Lambda.Russell.Inversion]
inv_typ_pi2 [in Lambda.Russell.Inversion]
inv_typ_pi2 [in Lambda.CCSum.Inversion]
inv_typ_prod [in Lambda.CCSum.Inversion]
inv_typ_prod [in Lambda.Russell.Inversion]
inv_typ_prod [in Lambda.Russell.Inversion]
inv_typ_prod2 [in Lambda.Russell.Inversion]
inv_typ_prod2 [in Lambda.Russell.Inversion]
inv_typ_prop [in Lambda.CCSum.Inversion]
inv_typ_prop [in Lambda.Russell.Inversion]
inv_typ_prop [in Lambda.Russell.Inversion]
inv_typ_ref [in Lambda.Russell.Inversion]
inv_typ_ref [in Lambda.Russell.Inversion]
inv_typ_ref [in Lambda.CCSum.Inversion]
inv_typ_set [in Lambda.CCSum.Inversion]
inv_typ_set [in Lambda.Russell.Inversion]
inv_typ_set [in Lambda.Russell.Inversion]
inv_typ_subset [in Lambda.CCSum.Inversion]
inv_typ_subset [in Lambda.Russell.Inversion]
inv_typ_subset [in Lambda.Russell.Inversion]
inv_typ_sum [in Lambda.CCSum.Inversion]
inv_typ_sum2 [in Lambda.Russell.Inversion]
inv_typ_sum2 [in Lambda.Russell.Inversion]
In_app [in Lambda.MyList]
in_set_not_sort [in Lambda.TPOSR.ChurchRosser]
is_conv [in Lambda.TPOSR.Conv_Dec]
is_conv [in Lambda.Conv_Dec]
is_low_full_lift [in Lambda.JRussell.GenerationCoerce]
is_low_lift [in Lambda.JRussell.GenerationCoerce]
item_ref_lift [in Lambda.JRussell.Thinning]
item_trunc [in Lambda.MyList]
item_unlab [in Lambda.Meta.TPOSR_JRussell]

---

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