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)

R

red [inductive, in Lambda.Reduction]
Reduction [library]
Reduction [library]
red1 [inductive, in Lambda.Reduction]
red1_env_hd [constructor, in Lambda.CCSum.SubjectReduction]
red1_env_tl [constructor, in Lambda.CCSum.SubjectReduction]
red1_exp_env_hd [constructor, in Lambda.CCSum.SubjectReduction]
red1_exp_env_tl [constructor, in Lambda.CCSum.SubjectReduction]
red1_exp_in_env [inductive, in Lambda.CCSum.SubjectReduction]
red1_in_env [inductive, in Lambda.CCSum.SubjectReduction]
red1_lift [lemma, in Lambda.Reduction]
red1_par_red1 [lemma, in Lambda.Reduction]
red1_red_ind [lemma, in Lambda.Reduction]
red1_subst_l [lemma, in Lambda.Reduction]
red1_subst_r [lemma, in Lambda.Reduction]
red_abs_abs [lemma, in Lambda.Reduction]
red_conv [lemma, in Lambda.Reduction]
red_env_hd [constructor, in Lambda.TPOSR.CtxReduction]
red_env_tl [constructor, in Lambda.TPOSR.CtxReduction]
red_in_env [inductive, in Lambda.TPOSR.CtxReduction]
red_item [lemma, in Lambda.TPOSR.CtxReduction]
red_item [lemma, in Lambda.CCSum.SubjectReduction]
red_normal [lemma, in Lambda.Reduction]
red_pair_pair [lemma, in Lambda.Reduction]
red_par_red [lemma, in Lambda.Reduction]
red_prod_prod [lemma, in Lambda.Reduction]
red_red1_ord_norm [lemma, in Lambda.Conv_Dec]
red_red_abs [lemma, in Lambda.Reduction]
red_red_app [lemma, in Lambda.Reduction]
red_red_pair [lemma, in Lambda.Reduction]
red_red_pi1 [lemma, in Lambda.Reduction]
red_red_pi2 [lemma, in Lambda.Reduction]
red_red_prod [lemma, in Lambda.Reduction]
red_red_subset [lemma, in Lambda.Reduction]
red_red_sum [lemma, in Lambda.Reduction]
red_ref_ref [lemma, in Lambda.Reduction]
red_sort_eq [lemma, in Lambda.JRussell.GenerationCoerce]
red_sort_eq [lemma, in Lambda.Russell.GenerationCoerce]
red_sort_mem [lemma, in Lambda.Reduction]
red_sort_sort [lemma, in Lambda.Reduction]
red_subset_subset [lemma, in Lambda.Reduction]
red_sum_sum [lemma, in Lambda.Reduction]
Ref [constructor, in Lambda.Terms]
refl_conv [constructor, in Lambda.Reduction]
refl_conv [constructor, in Lambda.TPOSR.Reduction]
refl_l [lemma, in Lambda.TPOSR.LeftReflexivity]
refl_lred [constructor, in Lambda.TPOSR.Reduction]
refl_par_lred1 [lemma, in Lambda.TPOSR.Reduction]
refl_par_red1 [lemma, in Lambda.Reduction]
refl_r [lemma, in Lambda.TPOSR.RightReflexivity]
refl_red [constructor, in Lambda.Reduction]
Ref_l [constructor, in Lambda.TPOSR.Terms]
ref_par_lred [constructor, in Lambda.TPOSR.Reduction]
ref_par_red [constructor, in Lambda.Reduction]
RightReflexivity [library]
russell_equiv_jrussell_conv [lemma, in Lambda.Meta.Russell_JRussell]
russell_equiv_jrussell_type [lemma, in Lambda.Meta.Russell_JRussell]
Russell_JRussell [library]
russell_subject_reduction [lemma, in Lambda.Meta.SubjectReduction]
russell_to_tposr [lemma, in Lambda.Meta.Russell_TPOSR]
Russell_TPOSR [library]
russell_unique_sort_conv [lemma, in Lambda.Meta.Russell_TPOSR]

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)