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

(90 entries)

Binder 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

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

D

D:17 [binder, in NbSteps.nb_steps]
D:19 [binder, in NbSteps.nb_steps]
D:21 [binder, in NbSteps.nb_steps]
D:25 [binder, in NbSteps.nb_steps]
D:30 [binder, in NbSteps.nb_steps]
D:33 [binder, in NbSteps.nb_steps]
D:39 [binder, in NbSteps.nb_steps]
D:45 [binder, in NbSteps.nb_steps]
D:48 [binder, in NbSteps.nb_steps]
D:51 [binder, in NbSteps.nb_steps]
D:55 [binder, in NbSteps.nb_steps]
D:58 [binder, in NbSteps.nb_steps]
D:66 [binder, in NbSteps.nb_steps]
D:69 [binder, in NbSteps.nb_steps]
D:71 [binder, in NbSteps.nb_steps]
D:75 [binder, in NbSteps.nb_steps]
D:77 [binder, in NbSteps.nb_steps]
D:79 [binder, in NbSteps.nb_steps]
D:83 [binder, in NbSteps.nb_steps]
D:85 [binder, in NbSteps.nb_steps]
D:88 [binder, in NbSteps.nb_steps]

E

e:12 [binder, in NbSteps.nb_steps]
e:16 [binder, in NbSteps.nb_steps]
e:28 [binder, in NbSteps.nb_steps]
E:44 [binder, in NbSteps.nb_steps]
E:62 [binder, in NbSteps.nb_steps]
E:65 [binder, in NbSteps.nb_steps]
E:74 [binder, in NbSteps.nb_steps]
E:76 [binder, in NbSteps.nb_steps]
E:82 [binder, in NbSteps.nb_steps]
E:84 [binder, in NbSteps.nb_steps]

G

G:23 [binder, in NbSteps.nb_steps]
G:36 [binder, in NbSteps.nb_steps]
G:42 [binder, in NbSteps.nb_steps]

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]
n:38 [binder, in NbSteps.nb_steps]
n:47 [binder, in NbSteps.nb_steps]
n:50 [binder, in NbSteps.nb_steps]
n:54 [binder, in NbSteps.nb_steps]
n:87 [binder, in NbSteps.nb_steps]

P

Pff:67 [binder, in NbSteps.nb_steps]
Ptt:63 [binder, in NbSteps.nb_steps]
P:60 [binder, in NbSteps.nb_steps]

T

true_false [lemma, in NbSteps.nb_steps]

X

x:13 [binder, in NbSteps.nb_steps]
x:18 [binder, in NbSteps.nb_steps]
x:20 [binder, in NbSteps.nb_steps]
x:24 [binder, in NbSteps.nb_steps]
x:29 [binder, in NbSteps.nb_steps]
x:32 [binder, in NbSteps.nb_steps]
x:37 [binder, in NbSteps.nb_steps]
x:4 [binder, in NbSteps.nb_steps]
x:43 [binder, in NbSteps.nb_steps]
x:46 [binder, in NbSteps.nb_steps]
x:49 [binder, in NbSteps.nb_steps]
x:53 [binder, in NbSteps.nb_steps]
x:57 [binder, in NbSteps.nb_steps]
x:59 [binder, in NbSteps.nb_steps]
x:61 [binder, in NbSteps.nb_steps]
x:64 [binder, in NbSteps.nb_steps]
x:68 [binder, in NbSteps.nb_steps]
x:7 [binder, in NbSteps.nb_steps]
x:70 [binder, in NbSteps.nb_steps]
x:78 [binder, in NbSteps.nb_steps]
x:8 [binder, in NbSteps.nb_steps]
x:86 [binder, in NbSteps.nb_steps]
x:9 [binder, 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]

---

Binder Index

D

D:17 [in NbSteps.nb_steps]
D:19 [in NbSteps.nb_steps]
D:21 [in NbSteps.nb_steps]
D:25 [in NbSteps.nb_steps]
D:30 [in NbSteps.nb_steps]
D:33 [in NbSteps.nb_steps]
D:39 [in NbSteps.nb_steps]
D:45 [in NbSteps.nb_steps]
D:48 [in NbSteps.nb_steps]
D:51 [in NbSteps.nb_steps]
D:55 [in NbSteps.nb_steps]
D:58 [in NbSteps.nb_steps]
D:66 [in NbSteps.nb_steps]
D:69 [in NbSteps.nb_steps]
D:71 [in NbSteps.nb_steps]
D:75 [in NbSteps.nb_steps]
D:77 [in NbSteps.nb_steps]
D:79 [in NbSteps.nb_steps]
D:83 [in NbSteps.nb_steps]
D:85 [in NbSteps.nb_steps]
D:88 [in NbSteps.nb_steps]

E

e:12 [in NbSteps.nb_steps]
e:16 [in NbSteps.nb_steps]
e:28 [in NbSteps.nb_steps]
E:44 [in NbSteps.nb_steps]
E:62 [in NbSteps.nb_steps]
E:65 [in NbSteps.nb_steps]
E:74 [in NbSteps.nb_steps]
E:76 [in NbSteps.nb_steps]
E:82 [in NbSteps.nb_steps]
E:84 [in NbSteps.nb_steps]

G

G:23 [in NbSteps.nb_steps]
G:36 [in NbSteps.nb_steps]
G:42 [in NbSteps.nb_steps]

N

n:38 [in NbSteps.nb_steps]
n:47 [in NbSteps.nb_steps]
n:50 [in NbSteps.nb_steps]
n:54 [in NbSteps.nb_steps]
n:87 [in NbSteps.nb_steps]

P

Pff:67 [in NbSteps.nb_steps]
Ptt:63 [in NbSteps.nb_steps]
P:60 [in NbSteps.nb_steps]

X

x:13 [in NbSteps.nb_steps]
x:18 [in NbSteps.nb_steps]
x:20 [in NbSteps.nb_steps]
x:24 [in NbSteps.nb_steps]
x:29 [in NbSteps.nb_steps]
x:32 [in NbSteps.nb_steps]
x:37 [in NbSteps.nb_steps]
x:4 [in NbSteps.nb_steps]
x:43 [in NbSteps.nb_steps]
x:46 [in NbSteps.nb_steps]
x:49 [in NbSteps.nb_steps]
x:53 [in NbSteps.nb_steps]
x:57 [in NbSteps.nb_steps]
x:59 [in NbSteps.nb_steps]
x:61 [in NbSteps.nb_steps]
x:64 [in NbSteps.nb_steps]
x:68 [in NbSteps.nb_steps]
x:7 [in NbSteps.nb_steps]
x:70 [in NbSteps.nb_steps]
x:78 [in NbSteps.nb_steps]
x:8 [in NbSteps.nb_steps]
x:86 [in NbSteps.nb_steps]
x:9 [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

(90 entries)

Binder 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

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