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

_

other

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

_

other

(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

_

other

(1 entry)

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

_

other

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

_

other

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

_

other

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

_

other

(1 entry)

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

_

other

(4 entries)

---

Global Index

I

is_𝔻ns_ff_π_intro [constructor, in NbSteps.nb_steps]
is_𝔻ns_ff_π [inductive, in NbSteps.nb_steps]
is_𝔻ns_ff_intro [constructor, in NbSteps.nb_steps]
is_𝔻ns_ff [inductive, in NbSteps.nb_steps]
is_𝔻ns_tt_intro [constructor, in NbSteps.nb_steps]
is_𝔻ns_tt [inductive, in NbSteps.nb_steps]

N

nb_steps [library]
ns [definition, in NbSteps.nb_steps]
nsa [definition, in NbSteps.nb_steps]
nsa_ns_n [lemma, in NbSteps.nb_steps]
nsa_ns_direct [lemma, in NbSteps.nb_steps]
nsa_ns_n_direct [lemma, in NbSteps.nb_steps]
ns_fix_ff [definition, in NbSteps.nb_steps]
ns_nsa.b [variable, in NbSteps.nb_steps]
ns_nsa.g [variable, in NbSteps.nb_steps]
ns_nsa.X [variable, in NbSteps.nb_steps]
ns_nsa [section, in NbSteps.nb_steps]

T

true_false [lemma, in NbSteps.nb_steps]

other

π_𝔻ns [definition, in NbSteps.nb_steps]
𝔻ns [inductive, in NbSteps.nb_steps]
𝔻ns_rect [lemma, in NbSteps.nb_steps]
𝔻ns_π_inv [lemma, in NbSteps.nb_steps]
𝔻ns_inv [lemma, in NbSteps.nb_steps]
𝔻ns_ff [constructor, in NbSteps.nb_steps]
𝔻ns_tt [constructor, in NbSteps.nb_steps]

---

Variable Index

N

ns_nsa.b [in NbSteps.nb_steps]
ns_nsa.g [in NbSteps.nb_steps]
ns_nsa.X [in NbSteps.nb_steps]

---

Library Index

N

nb_steps

---

Lemma Index

N

nsa_ns_n [in NbSteps.nb_steps]
nsa_ns_direct [in NbSteps.nb_steps]
nsa_ns_n_direct [in NbSteps.nb_steps]

T

true_false [in NbSteps.nb_steps]

other

𝔻ns_rect [in NbSteps.nb_steps]
𝔻ns_π_inv [in NbSteps.nb_steps]
𝔻ns_inv [in NbSteps.nb_steps]

---

Constructor Index

I

is_𝔻ns_ff_π_intro [in NbSteps.nb_steps]
is_𝔻ns_ff_intro [in NbSteps.nb_steps]
is_𝔻ns_tt_intro [in NbSteps.nb_steps]

other

𝔻ns_ff [in NbSteps.nb_steps]
𝔻ns_tt [in NbSteps.nb_steps]

---

Inductive Index

I

is_𝔻ns_ff_π [in NbSteps.nb_steps]
is_𝔻ns_ff [in NbSteps.nb_steps]
is_𝔻ns_tt [in NbSteps.nb_steps]

other

𝔻ns [in NbSteps.nb_steps]

---

Section Index

N

ns_nsa [in NbSteps.nb_steps]

---

Definition Index

N

ns [in NbSteps.nb_steps]
nsa [in NbSteps.nb_steps]
ns_fix_ff [in NbSteps.nb_steps]

other

π_𝔻ns [in NbSteps.nb_steps]

---

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

_

other

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

_

other

(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

_

other

(1 entry)

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

_

other

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

_

other

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

_

other

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

_

other

(1 entry)

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

_

other

(4 entries)

---

This page has been generated by coqdoc