Lambda.Meta.SubjectReduction

Global Index

H

Q

X

Y

Z

_

(1755 entries)

Lemma Index

B

H

Q

X

Y

Z

_

(1070 entries)

Section Index

A

B

D

E

F

G

H

I

J

K

M

O

P

Q

R

S

U

V

W

X

Y

Z

_

(6 entries)

Constructor Index

G

H

L

O

Q

U

V

X

Y

Z

_

(426 entries)

Inductive Index

A

B

D

G

H

K

N

O

Q

U

V

X

Y

Z

_

(81 entries)

Definition Index

A

B

G

H

J

K

Q

R

V

W

X

Y

Z

_

(73 entries)

Variable Index

A

B

C

D

E

F

G

H

I

J

K

M

N

O

P

Q

R

S

U

V

W

X

Y

Z

_

(3 entries)

Library Index

A

H

K

O

Q

W

X

Y

Z

_

(96 entries)

I

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

Global Index

H

Q

X

Y

Z

_

(1755 entries)

Lemma Index

B

H

Q

X

Y

Z

_

(1070 entries)

Section Index

A

B

D

E

F

G

H

I

J

K

M

O

P

Q

R

S

U

V

W

X

Y

Z

_

(6 entries)

Constructor Index

G

H

L

O

Q

U

V

X

Y

Z

_

(426 entries)

Inductive Index

A

B

D

G

H

K

N

O

Q

U

V

X

Y

Z

_

(81 entries)

Definition Index

A

B

G

H

J

K

Q

R

V

W

X

Y

Z

_

(73 entries)

Variable Index

A

B

C

D

E

F

G

H

I

J

K

M

N

O

P

Q

R

S

U

V

W

X

Y

Z

_

(3 entries)

Library Index

A

H

K

O

Q

W

X

Y

Z

_

(96 entries)