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

(2881 entries)

Notation 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

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

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

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

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

_

other

(332 entries)

Axiom 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

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

(21 entries)

Projection 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)

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

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

_

other

(98 entries)

Record 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

(2 entries)

---

Global Index

A

acc:149 [binder, in GMu.Prelude]
acc:151 [binder, in GMu.Prelude]
acc:153 [binder, in GMu.Prelude]
acc:155 [binder, in GMu.Prelude]
acc:20 [binder, in GMu.Equations]
acc:22 [binder, in GMu.Equations]
acc:24 [binder, in GMu.Equations]
acc:26 [binder, in GMu.Equations]
acc:295 [binder, in GMu.Definitions]
Ah:132 [binder, in GMu.Prelude]
all_distinct [axiom, in GMu.TestVector]
all_distinct [lemma, in GMu.Tests2]
all_distinct [axiom, in GMu.TestEquality]
Alphas:106 [binder, in GMu.Regularity]
Alphas:227 [binder, in GMu.Definitions]
Alphas:355 [binder, in GMu.Definitions]
Alphas:359 [binder, in GMu.Definitions]
Alphas:508 [binder, in GMu.Definitions]
Alphas:75 [binder, in GMu.Prelude]
alpha:358 [binder, in GMu.Definitions]
alpha:362 [binder, in GMu.Definitions]
args:143 [binder, in GMu.Definitions]
args:147 [binder, in GMu.Definitions]
args:151 [binder, in GMu.Definitions]
args:153 [binder, in GMu.Definitions]
argT:352 [binder, in GMu.Definitions]
Arity:320 [binder, in GMu.Definitions]
Arity:367 [binder, in GMu.Definitions]
As:106 [binder, in GMu.Zip]
As:112 [binder, in GMu.Zip]
As:119 [binder, in GMu.InfrastructureFV]
As:125 [binder, in GMu.InfrastructureOpen]
As:137 [binder, in GMu.InfrastructureOpen]
As:138 [binder, in GMu.Preservation]
As:153 [binder, in GMu.InfrastructureFV]
As:158 [binder, in GMu.InfrastructureSubst]
As:162 [binder, in GMu.InfrastructureSubst]
As:162 [binder, in GMu.InfrastructureFV]
As:169 [binder, in GMu.InfrastructureFV]
As:172 [binder, in GMu.InfrastructureSubst]
As:176 [binder, in GMu.InfrastructureSubst]
As:181 [binder, in GMu.InfrastructureFV]
As:197 [binder, in GMu.Preservation]
As:209 [binder, in GMu.SubstMatch]
As:27 [binder, in GMu.Equations]
As:272 [binder, in GMu.Definitions]
As:29 [binder, in GMu.Regularity2]
As:29 [binder, in GMu.Preservation]
As:30 [binder, in GMu.Equations]
As:34 [binder, in GMu.Zip]
As:35 [binder, in GMu.Regularity]
As:35 [binder, in GMu.Equations]
As:41 [binder, in GMu.Zip]
As:49 [binder, in GMu.Zip]
As:56 [binder, in GMu.Zip]
As:62 [binder, in GMu.Zip]
As:69 [binder, in GMu.InfrastructureFV]
As:70 [binder, in GMu.Zip]
As:77 [binder, in GMu.Zip]
As:83 [binder, in GMu.Zip]
As:90 [binder, in GMu.Zip]
As:93 [binder, in GMu.InfrastructureOpen]
As:96 [binder, in GMu.Prelude]
As:99 [binder, in GMu.Regularity]
Ats:133 [binder, in GMu.Prelude]
AT:102 [binder, in GMu.Zip]
AT:108 [binder, in GMu.Zip]
AT:47 [binder, in GMu.Zip]
AT:54 [binder, in GMu.Zip]
AT:60 [binder, in GMu.Zip]
AT:68 [binder, in GMu.Zip]
AT:75 [binder, in GMu.Zip]
AT:81 [binder, in GMu.Zip]
AT:88 [binder, in GMu.Zip]
A:1 [binder, in GMu.InfrastructureFV]
A:10 [binder, in GMu.TestVector]
a:101 [binder, in GMu.Zip]
A:104 [binder, in GMu.Zip]
A:104 [binder, in GMu.Definitions]
A:105 [binder, in GMu.SubstMatch]
A:107 [binder, in GMu.Prelude]
A:109 [binder, in GMu.Regularity]
A:110 [binder, in GMu.Zip]
A:110 [binder, in GMu.SubstMatch]
A:110 [binder, in GMu.Regularity]
A:112 [binder, in GMu.Prelude]
A:117 [binder, in GMu.Preservation]
a:118 [binder, in GMu.Prelude]
A:118 [binder, in GMu.Preservation]
a:120 [binder, in GMu.Prelude]
A:122 [binder, in GMu.Prelude]
A:125 [binder, in GMu.Regularity]
A:126 [binder, in GMu.Regularity]
A:129 [binder, in GMu.Prelude]
A:138 [binder, in GMu.Prelude]
A:14 [binder, in GMu.TestCommon]
A:142 [binder, in GMu.Prelude]
A:146 [binder, in GMu.Prelude]
A:149 [binder, in GMu.Preservation]
A:149 [binder, in GMu.InfrastructureFV]
A:150 [binder, in GMu.Preservation]
A:151 [binder, in GMu.Preservation]
A:152 [binder, in GMu.Preservation]
A:153 [binder, in GMu.Preservation]
A:154 [binder, in GMu.InfrastructureFV]
A:155 [binder, in GMu.Preservation]
A:157 [binder, in GMu.Prelude]
A:160 [binder, in GMu.Prelude]
A:161 [binder, in GMu.InfrastructureSubst]
a:165 [binder, in GMu.Prelude]
A:167 [binder, in GMu.InfrastructureSubst]
A:167 [binder, in GMu.InfrastructureFV]
A:172 [binder, in GMu.Prelude]
A:174 [binder, in GMu.InfrastructureSubst]
A:176 [binder, in GMu.Prelude]
A:177 [binder, in GMu.InfrastructureFV]
A:178 [binder, in GMu.InfrastructureSubst]
A:181 [binder, in GMu.InfrastructureSubst]
A:183 [binder, in GMu.Prelude]
A:19 [binder, in GMu.TestCommon]
A:20 [binder, in GMu.InfrastructureFV]
A:200 [binder, in GMu.Preservation]
A:208 [binder, in GMu.Preservation]
A:209 [binder, in GMu.Preservation]
a:21 [binder, in GMu.Zip]
A:229 [binder, in GMu.Definitions]
A:233 [binder, in GMu.SubstMatch]
a:25 [binder, in GMu.Zip]
A:25 [binder, in GMu.InfrastructureSubstPrim]
A:28 [binder, in GMu.Equations]
A:283 [binder, in GMu.Definitions]
a:29 [binder, in GMu.Zip]
a:3 [binder, in GMu.TestCommon]
A:30 [binder, in GMu.InfrastructureSubst]
A:31 [binder, in GMu.Regularity2]
A:32 [binder, in GMu.Regularity2]
A:33 [binder, in GMu.Regularity2]
A:33 [binder, in GMu.Preservation]
A:332 [binder, in GMu.Definitions]
A:34 [binder, in GMu.Equations]
A:34 [binder, in GMu.Preservation]
A:35 [binder, in GMu.TestCommon]
A:36 [binder, in GMu.InfrastructureSubst]
A:37 [binder, in GMu.Zip]
A:38 [binder, in GMu.Regularity]
A:39 [binder, in GMu.Equations]
A:4 [binder, in GMu.InfrastructureSubstPrim]
A:42 [binder, in GMu.Equations]
A:42 [binder, in GMu.InfrastructureFV]
A:43 [binder, in GMu.Preservation]
a:44 [binder, in GMu.Zip]
A:44 [binder, in GMu.Prelude]
A:44 [binder, in GMu.Preservation]
A:46 [binder, in GMu.Zip]
A:46 [binder, in GMu.Equations]
A:48 [binder, in GMu.Prelude]
A:5 [binder, in GMu.TestVector]
A:510 [binder, in GMu.Definitions]
A:52 [binder, in GMu.Zip]
A:52 [binder, in GMu.SubstMatch]
a:53 [binder, in GMu.Prelude]
A:55 [binder, in GMu.Prelude]
A:575 [binder, in GMu.Definitions]
A:58 [binder, in GMu.Zip]
A:6 [binder, in GMu.TestVector]
a:6 [binder, in GMu.TestCommon]
a:63 [binder, in GMu.Prelude]
a:65 [binder, in GMu.Prelude]
A:66 [binder, in GMu.Zip]
A:67 [binder, in GMu.Prelude]
A:69 [binder, in GMu.SubstMatch]
A:69 [binder, in GMu.Equations]
A:7 [binder, in GMu.TestCommon]
A:70 [binder, in GMu.Prelude]
A:72 [binder, in GMu.Zip]
A:76 [binder, in GMu.Prelude]
A:77 [binder, in GMu.Prelude]
a:78 [binder, in GMu.Prelude]
A:79 [binder, in GMu.Zip]
A:79 [binder, in GMu.Prelude]
A:80 [binder, in GMu.Preservation]
A:81 [binder, in GMu.Preservation]
A:85 [binder, in GMu.Zip]
A:92 [binder, in GMu.Zip]
A:93 [binder, in GMu.Prelude]
A:96 [binder, in GMu.Zip]
A:98 [binder, in GMu.Prelude]
A:99 [binder, in GMu.SubstMatch]
A:99 [binder, in GMu.Prelude]

B

base:10 [binder, in GMu.InfrastructureFV]
base:15 [binder, in GMu.InfrastructureFV]
base:25 [binder, in GMu.InfrastructureFV]
base:31 [binder, in GMu.InfrastructureFV]
base:39 [binder, in GMu.InfrastructureFV]
base:5 [binder, in GMu.InfrastructureFV]
bind [inductive, in GMu.Definitions]
binds_ext [lemma, in GMu.Prelude]
bind_var [constructor, in GMu.Definitions]
Bs:107 [binder, in GMu.Zip]
Bs:113 [binder, in GMu.Zip]
Bs:35 [binder, in GMu.Zip]
Bs:42 [binder, in GMu.Zip]
Bs:50 [binder, in GMu.Zip]
Bs:57 [binder, in GMu.Zip]
Bs:63 [binder, in GMu.Zip]
Bs:71 [binder, in GMu.Zip]
Bs:78 [binder, in GMu.Zip]
Bs:84 [binder, in GMu.Zip]
Bs:91 [binder, in GMu.Zip]
BT:103 [binder, in GMu.Zip]
BT:109 [binder, in GMu.Zip]
BT:48 [binder, in GMu.Zip]
BT:55 [binder, in GMu.Zip]
BT:61 [binder, in GMu.Zip]
BT:69 [binder, in GMu.Zip]
BT:76 [binder, in GMu.Zip]
BT:82 [binder, in GMu.Zip]
BT:89 [binder, in GMu.Zip]
b:100 [binder, in GMu.Zip]
B:100 [binder, in GMu.SubstMatch]
B:100 [binder, in GMu.Prelude]
B:105 [binder, in GMu.Zip]
B:111 [binder, in GMu.Zip]
B:113 [binder, in GMu.Prelude]
b:119 [binder, in GMu.Prelude]
b:121 [binder, in GMu.Prelude]
B:139 [binder, in GMu.Prelude]
B:143 [binder, in GMu.Prelude]
B:147 [binder, in GMu.Prelude]
B:158 [binder, in GMu.Prelude]
B:161 [binder, in GMu.Prelude]
B:163 [binder, in GMu.InfrastructureFV]
b:166 [binder, in GMu.Prelude]
B:170 [binder, in GMu.InfrastructureFV]
B:177 [binder, in GMu.Prelude]
B:20 [binder, in GMu.TestCommon]
b:22 [binder, in GMu.Zip]
b:26 [binder, in GMu.Zip]
b:266 [binder, in GMu.Definitions]
b:274 [binder, in GMu.Definitions]
b:30 [binder, in GMu.Zip]
B:36 [binder, in GMu.Zip]
B:36 [binder, in GMu.TestCommon]
b:4 [binder, in GMu.TestCommon]
B:40 [binder, in GMu.Equations]
B:43 [binder, in GMu.Zip]
B:43 [binder, in GMu.Equations]
B:43 [binder, in GMu.InfrastructureFV]
b:45 [binder, in GMu.Zip]
B:47 [binder, in GMu.Equations]
B:49 [binder, in GMu.Prelude]
B:53 [binder, in GMu.Zip]
B:56 [binder, in GMu.Prelude]
B:58 [binder, in GMu.Prelude]
B:59 [binder, in GMu.Zip]
b:64 [binder, in GMu.Prelude]
B:65 [binder, in GMu.Zip]
b:66 [binder, in GMu.Prelude]
B:73 [binder, in GMu.Zip]
B:8 [binder, in GMu.TestCommon]
B:80 [binder, in GMu.Zip]
B:80 [binder, in GMu.Prelude]
B:86 [binder, in GMu.Zip]
B:93 [binder, in GMu.Zip]
B:94 [binder, in GMu.Prelude]
B:97 [binder, in GMu.Zip]

C

CanonicalConstructorType [lemma, in GMu.CanonicalForms]
CanonicalConstructorTypeGen [lemma, in GMu.CanonicalForms]
CanonicalFormAbs [lemma, in GMu.CanonicalForms]
CanonicalFormGadt [lemma, in GMu.CanonicalForms]
CanonicalForms [library]
CanonicalFormTAbs [lemma, in GMu.CanonicalForms]
CanonicalFormTuple [lemma, in GMu.CanonicalForms]
CanonicalFormUnit [lemma, in GMu.CanonicalForms]
Cargtype [projection, in GMu.Definitions]
CargType:408 [binder, in GMu.Definitions]
CargType:96 [binder, in GMu.Regularity]
Carity [projection, in GMu.Definitions]
Carity:351 [binder, in GMu.Definitions]
Carity:407 [binder, in GMu.Definitions]
Carity:542 [binder, in GMu.Definitions]
Carity:95 [binder, in GMu.Regularity]
Ce:543 [binder, in GMu.Definitions]
cid:539 [binder, in GMu.Definitions]
clArity:39 [binder, in GMu.Definitions]
clause [constructor, in GMu.Definitions]
Clause [inductive, in GMu.Definitions]
clauseArity [definition, in GMu.Definitions]
Clauses:186 [binder, in GMu.Prelude]
clauses:77 [binder, in GMu.Definitions]
clauses:87 [binder, in GMu.Definitions]
clauseTerm [definition, in GMu.Definitions]
clause:4 [binder, in GMu.Progress]
clause:505 [binder, in GMu.Definitions]
clause:507 [binder, in GMu.Definitions]
clause:6 [binder, in GMu.Progress]
clA:189 [binder, in GMu.Prelude]
closed_term_match [constructor, in GMu.InfrastructureOpen]
closed_term_constructor [constructor, in GMu.InfrastructureOpen]
closed_trm_let [constructor, in GMu.InfrastructureOpen]
closed_trm_fix [constructor, in GMu.InfrastructureOpen]
closed_trm_tapp [constructor, in GMu.InfrastructureOpen]
closed_trm_tabs [constructor, in GMu.InfrastructureOpen]
closed_trm_app [constructor, in GMu.InfrastructureOpen]
closed_trm_abs [constructor, in GMu.InfrastructureOpen]
closed_trm_tuple [constructor, in GMu.InfrastructureOpen]
closed_trm_snd [constructor, in GMu.InfrastructureOpen]
closed_trm_fst [constructor, in GMu.InfrastructureOpen]
closed_trm_unit [constructor, in GMu.InfrastructureOpen]
closed_trm_fvar [constructor, in GMu.InfrastructureOpen]
closed_trm_bvar [constructor, in GMu.InfrastructureOpen]
closed_id [lemma, in GMu.InfrastructureOpen]
closed_typ_gadt [constructor, in GMu.InfrastructureOpen]
closed_typ_all [constructor, in GMu.InfrastructureOpen]
closed_typ_arrow [constructor, in GMu.InfrastructureOpen]
closed_typ_tuple [constructor, in GMu.InfrastructureOpen]
closed_typ_unit [constructor, in GMu.InfrastructureOpen]
closed_typ_fvar [constructor, in GMu.InfrastructureOpen]
closed_typ_bvar [constructor, in GMu.InfrastructureOpen]
clT:190 [binder, in GMu.Prelude]
cl:17 [binder, in GMu.InfrastructureFV]
cl:18 [binder, in GMu.InfrastructureFV]
cl:188 [binder, in GMu.Prelude]
cl:19 [binder, in GMu.InfrastructureFV]
cl:226 [binder, in GMu.Definitions]
cl:29 [binder, in GMu.InfrastructureFV]
cl:33 [binder, in GMu.InfrastructureFV]
cl:34 [binder, in GMu.InfrastructureFV]
cl:35 [binder, in GMu.InfrastructureFV]
cl:83 [binder, in GMu.InfrastructureOpen]
coerce_types [lemma, in GMu.TestEquality]
coerce_trm [definition, in GMu.TestEquality]
coerce_typ [definition, in GMu.TestEquality]
cons [definition, in GMu.TestVector]
Cons [definition, in GMu.TestVector]
const [definition, in GMu.Tests2]
construct_types [lemma, in GMu.TestEquality]
construct_trm [definition, in GMu.TestEquality]
construct_typ [definition, in GMu.TestEquality]
const_test_evals [lemma, in GMu.Tests2]
const_test_types [lemma, in GMu.Tests2]
const_test [definition, in GMu.Tests2]
const_types [lemma, in GMu.Tests2]
cons_type [lemma, in GMu.TestVector]
contradictory_env_test [lemma, in GMu.Equations]
contradictory_env_test_0 [lemma, in GMu.Equations]
contradictory_bounds [definition, in GMu.Definitions]
Crettypes [projection, in GMu.Definitions]
CretTypes:409 [binder, in GMu.Definitions]
CretTypes:97 [binder, in GMu.Regularity]
cs:106 [binder, in GMu.Definitions]
cs:109 [binder, in GMu.Definitions]
Ctors:406 [binder, in GMu.Definitions]
Ctors:93 [binder, in GMu.Regularity]
Ctor:14 [binder, in GMu.CanonicalForms]
Ctor:403 [binder, in GMu.Definitions]
Ctor:549 [binder, in GMu.Definitions]
Ctor:6 [binder, in GMu.CanonicalForms]
Ctor:94 [binder, in GMu.Regularity]
ctx [definition, in GMu.Definitions]
c:101 [binder, in GMu.SubstMatch]
C:101 [binder, in GMu.Prelude]
c:107 [binder, in GMu.Definitions]
c:110 [binder, in GMu.Definitions]
c:128 [binder, in GMu.Definitions]
C:133 [binder, in GMu.InfrastructureFV]
c:135 [binder, in GMu.Definitions]
C:140 [binder, in GMu.Prelude]
C:159 [binder, in GMu.Prelude]
C:16 [binder, in GMu.Zip]
c:171 [binder, in GMu.Definitions]
C:37 [binder, in GMu.TestCommon]
c:41 [binder, in GMu.Definitions]
c:43 [binder, in GMu.Definitions]
C:46 [binder, in GMu.CanonicalForms]
C:48 [binder, in GMu.Equations]
c:5 [binder, in GMu.TestCommon]
C:57 [binder, in GMu.Prelude]
c:80 [binder, in GMu.Definitions]
C:81 [binder, in GMu.Prelude]
c:88 [binder, in GMu.Definitions]
C:9 [binder, in GMu.Zip]
c:9 [binder, in GMu.TestCommon]
c:91 [binder, in GMu.Definitions]
c:92 [binder, in GMu.Definitions]
c:94 [binder, in GMu.Definitions]
C:95 [binder, in GMu.Prelude]

D

Definitions [library]
DefinitionsTests [library]
Defs:185 [binder, in GMu.Prelude]
Defs:321 [binder, in GMu.Definitions]
Defs:368 [binder, in GMu.Definitions]
Defs:502 [binder, in GMu.Definitions]
def:187 [binder, in GMu.Prelude]
def:3 [binder, in GMu.Progress]
Def:369 [binder, in GMu.Definitions]
def:5 [binder, in GMu.Progress]
def:504 [binder, in GMu.Definitions]
def:506 [binder, in GMu.Definitions]
Deqs:140 [binder, in GMu.InfrastructureFV]
Deqs:20 [binder, in GMu.Preservation]
Deqs:22 [binder, in GMu.Regularity2]
Deqs:29 [binder, in GMu.Regularity]
destruct_types [lemma, in GMu.TestEquality]
destruct_trm [definition, in GMu.TestEquality]
destruct_typ [definition, in GMu.TestEquality]
distinctive_cons [constructor, in GMu.Definitions]
distinctive_empty [constructor, in GMu.Definitions]
DistinctList [inductive, in GMu.Definitions]
distinct_split1 [lemma, in GMu.InfrastructureFV]
divergent [definition, in GMu.Tests]
divergent_diverges [lemma, in GMu.Tests]
divergent_type [lemma, in GMu.Tests]
domDelta_subst_td [lemma, in GMu.InfrastructureFV]
domDelta_app [lemma, in GMu.InfrastructureFV]
domDelta_in [lemma, in GMu.InfrastructureFV]
domΔ [definition, in GMu.Definitions]
D':89 [binder, in GMu.SubstMatch]
D1:10 [binder, in GMu.Regularity2]
D1:11 [binder, in GMu.SubstMatch]
D1:11 [binder, in GMu.Preservation]
D1:14 [binder, in GMu.Regularity]
D1:15 [binder, in GMu.Regularity2]
D1:151 [binder, in GMu.InfrastructureFV]
D1:173 [binder, in GMu.InfrastructureFV]
D1:20 [binder, in GMu.Regularity2]
D1:23 [binder, in GMu.Regularity]
D1:230 [binder, in GMu.SubstMatch]
D1:24 [binder, in GMu.SubstMatch]
D1:27 [binder, in GMu.Regularity2]
D1:28 [binder, in GMu.Regularity]
D1:3 [binder, in GMu.Preservation]
D1:35 [binder, in GMu.Regularity2]
D1:35 [binder, in GMu.SubstMatch]
D1:41 [binder, in GMu.Regularity2]
D1:41 [binder, in GMu.SubstMatch]
D1:59 [binder, in GMu.SubstMatch]
D1:6 [binder, in GMu.Regularity2]
D1:6 [binder, in GMu.SubstMatch]
D1:62 [binder, in GMu.Regularity]
D1:65 [binder, in GMu.Regularity2]
D1:74 [binder, in GMu.SubstMatch]
D1:76 [binder, in GMu.Regularity]
D1:79 [binder, in GMu.Regularity2]
D1:79 [binder, in GMu.SubstMatch]
D1:81 [binder, in GMu.Regularity]
D1:92 [binder, in GMu.InfrastructureFV]
D1:95 [binder, in GMu.InfrastructureFV]
D2:11 [binder, in GMu.Regularity2]
D2:116 [binder, in GMu.SubstMatch]
D2:12 [binder, in GMu.SubstMatch]
D2:12 [binder, in GMu.Preservation]
D2:15 [binder, in GMu.Regularity]
D2:152 [binder, in GMu.InfrastructureFV]
D2:16 [binder, in GMu.Regularity2]
D2:174 [binder, in GMu.InfrastructureFV]
D2:21 [binder, in GMu.Regularity2]
D2:232 [binder, in GMu.SubstMatch]
D2:24 [binder, in GMu.Regularity]
D2:26 [binder, in GMu.SubstMatch]
D2:28 [binder, in GMu.Regularity2]
D2:30 [binder, in GMu.Regularity]
D2:36 [binder, in GMu.Regularity2]
D2:37 [binder, in GMu.SubstMatch]
D2:4 [binder, in GMu.Preservation]
D2:42 [binder, in GMu.Regularity2]
D2:42 [binder, in GMu.SubstMatch]
D2:60 [binder, in GMu.SubstMatch]
D2:63 [binder, in GMu.Regularity]
D2:66 [binder, in GMu.Regularity2]
D2:7 [binder, in GMu.Regularity2]
D2:7 [binder, in GMu.SubstMatch]
D2:75 [binder, in GMu.SubstMatch]
D2:77 [binder, in GMu.Regularity]
D2:80 [binder, in GMu.Regularity2]
D2:80 [binder, in GMu.SubstMatch]
D2:82 [binder, in GMu.Regularity]
D2:93 [binder, in GMu.InfrastructureFV]
D2:96 [binder, in GMu.InfrastructureFV]
D3:32 [binder, in GMu.SubstMatch]
D3:78 [binder, in GMu.Regularity]
D4:33 [binder, in GMu.SubstMatch]
D:167 [binder, in GMu.Prelude]
d:181 [binder, in GMu.Prelude]
D:19 [binder, in GMu.SubstMatch]
D:2 [binder, in GMu.Regularity2]
D:2 [binder, in GMu.SubstMatch]
D:224 [binder, in GMu.SubstMatch]
D:38 [binder, in GMu.TestCommon]
D:49 [binder, in GMu.Equations]
d:577 [binder, in GMu.Definitions]
d:581 [binder, in GMu.Definitions]
D:85 [binder, in GMu.SubstMatch]
D:90 [binder, in GMu.SubstMatch]

E

empty_eq_is_equivalent [lemma, in GMu.Equations]
empty_is_not_contradictory [lemma, in GMu.Equations]
empty_inter_implies_notin [lemma, in GMu.Prelude]
emptyΔ [definition, in GMu.Definitions]
entails_through_subst [lemma, in GMu.SubstMatch]
entails_semantic [definition, in GMu.Definitions]
env_map_compose [lemma, in GMu.Prelude]
Eq [axiom, in GMu.TestEquality]
EqDef [definition, in GMu.TestEquality]
Equations [library]
equations_weaken_match [lemma, in GMu.SubstMatch]
equations_from_lists_map [lemma, in GMu.Equations]
equations_from_lists_are_equations [lemma, in GMu.Prelude]
equations_from_lists [definition, in GMu.Definitions]
equations_have_no_dom [lemma, in GMu.InfrastructureFV]
equation_strengthen [lemma, in GMu.SubstMatch]
equation_weaken_var [lemma, in GMu.SubstMatch]
equation_weaken_eq [lemma, in GMu.SubstMatch]
eq_dec_var [lemma, in GMu.Prelude]
eq_typ_tuple [lemma, in GMu.TestCommon]
eq_typ_gadt [lemma, in GMu.TestCommon]
eq:141 [binder, in GMu.InfrastructureFV]
eq:170 [binder, in GMu.Prelude]
eq:18 [binder, in GMu.Regularity2]
eq:24 [binder, in GMu.Regularity2]
eq:24 [binder, in GMu.Preservation]
eq:284 [binder, in GMu.Definitions]
eq:32 [binder, in GMu.Regularity]
eq:340 [binder, in GMu.Definitions]
eq:7 [binder, in GMu.Preservation]
eq:82 [binder, in GMu.Regularity2]
ered_match [constructor, in GMu.Definitions]
ered_let [constructor, in GMu.Definitions]
ered_tuple_snd [constructor, in GMu.Definitions]
ered_tuple_fst [constructor, in GMu.Definitions]
ered_snd [constructor, in GMu.Definitions]
ered_fst [constructor, in GMu.Definitions]
ered_tapp [constructor, in GMu.Definitions]
ered_app_2 [constructor, in GMu.Definitions]
ered_constructor [constructor, in GMu.Definitions]
ered_app_1 [constructor, in GMu.Definitions]
evals [inductive, in GMu.TestCommon]
eval_finish [constructor, in GMu.TestCommon]
eval_step [constructor, in GMu.TestCommon]
exist_alphas [lemma, in GMu.Prelude]
ext_in_map [lemma, in GMu.Prelude]
e':27 [binder, in GMu.InfrastructureFV]
e':5 [binder, in GMu.Tests]
e':523 [binder, in GMu.Definitions]
e':526 [binder, in GMu.Definitions]
e':529 [binder, in GMu.Definitions]
e':536 [binder, in GMu.Definitions]
e':544 [binder, in GMu.Definitions]
e':551 [binder, in GMu.Definitions]
e':559 [binder, in GMu.Definitions]
e':561 [binder, in GMu.Definitions]
e':587 [binder, in GMu.Definitions]
e':592 [binder, in GMu.Definitions]
E0:106 [binder, in GMu.Preservation]
E0:112 [binder, in GMu.Preservation]
E0:57 [binder, in GMu.Preservation]
E0:63 [binder, in GMu.Preservation]
E0:69 [binder, in GMu.Preservation]
E0:75 [binder, in GMu.Preservation]
E0:83 [binder, in GMu.Preservation]
E0:89 [binder, in GMu.Preservation]
e1':546 [binder, in GMu.Definitions]
e1':556 [binder, in GMu.Definitions]
e1':564 [binder, in GMu.Definitions]
e1':570 [binder, in GMu.Definitions]
e1':574 [binder, in GMu.Definitions]
e1:115 [binder, in GMu.InfrastructureSubst]
e1:119 [binder, in GMu.InfrastructureSubst]
e1:15 [binder, in GMu.CanonicalForms]
e1:184 [binder, in GMu.InfrastructureSubst]
e1:187 [binder, in GMu.InfrastructureSubst]
e1:195 [binder, in GMu.Definitions]
e1:197 [binder, in GMu.Definitions]
e1:199 [binder, in GMu.Definitions]
e1:200 [binder, in GMu.Definitions]
e1:203 [binder, in GMu.Definitions]
e1:205 [binder, in GMu.Definitions]
e1:208 [binder, in GMu.Definitions]
e1:219 [binder, in GMu.Definitions]
e1:223 [binder, in GMu.Definitions]
e1:231 [binder, in GMu.Definitions]
e1:232 [binder, in GMu.Definitions]
e1:234 [binder, in GMu.Definitions]
e1:238 [binder, in GMu.Definitions]
e1:404 [binder, in GMu.Definitions]
e1:418 [binder, in GMu.Definitions]
e1:427 [binder, in GMu.Definitions]
e1:435 [binder, in GMu.Definitions]
e1:443 [binder, in GMu.Definitions]
e1:453 [binder, in GMu.Definitions]
e1:462 [binder, in GMu.Definitions]
e1:469 [binder, in GMu.Definitions]
e1:486 [binder, in GMu.Definitions]
e1:521 [binder, in GMu.Definitions]
e1:524 [binder, in GMu.Definitions]
e1:537 [binder, in GMu.Definitions]
e1:545 [binder, in GMu.Definitions]
e1:55 [binder, in GMu.InfrastructureOpen]
e1:555 [binder, in GMu.Definitions]
e1:562 [binder, in GMu.Definitions]
e1:568 [binder, in GMu.Definitions]
e1:571 [binder, in GMu.Definitions]
e1:61 [binder, in GMu.InfrastructureOpen]
e1:7 [binder, in GMu.CanonicalForms]
e1:72 [binder, in GMu.InfrastructureOpen]
e2':554 [binder, in GMu.Definitions]
e2':567 [binder, in GMu.Definitions]
e2:117 [binder, in GMu.InfrastructureSubst]
e2:121 [binder, in GMu.InfrastructureSubst]
e2:186 [binder, in GMu.InfrastructureSubst]
e2:189 [binder, in GMu.InfrastructureSubst]
e2:198 [binder, in GMu.Definitions]
e2:206 [binder, in GMu.Definitions]
e2:220 [binder, in GMu.Definitions]
e2:235 [binder, in GMu.Definitions]
e2:428 [binder, in GMu.Definitions]
e2:454 [binder, in GMu.Definitions]
e2:487 [binder, in GMu.Definitions]
e2:528 [binder, in GMu.Definitions]
e2:547 [binder, in GMu.Definitions]
e2:553 [binder, in GMu.Definitions]
e2:56 [binder, in GMu.InfrastructureOpen]
e2:563 [binder, in GMu.Definitions]
e2:566 [binder, in GMu.Definitions]
e2:569 [binder, in GMu.Definitions]
e2:62 [binder, in GMu.InfrastructureOpen]
e2:73 [binder, in GMu.InfrastructureOpen]
e:1 [binder, in GMu.Prelude]
e:1 [binder, in GMu.InfrastructureOpen]
e:100 [binder, in GMu.InfrastructureSubst]
e:101 [binder, in GMu.Preservation]
E:102 [binder, in GMu.Prelude]
e:102 [binder, in GMu.InfrastructureOpen]
e:105 [binder, in GMu.InfrastructureSubst]
e:109 [binder, in GMu.InfrastructureSubst]
E:111 [binder, in GMu.Prelude]
e:112 [binder, in GMu.Definitions]
e:112 [binder, in GMu.InfrastructureSubst]
e:112 [binder, in GMu.InfrastructureOpen]
e:115 [binder, in GMu.InfrastructureOpen]
E:118 [binder, in GMu.InfrastructureFV]
E:119 [binder, in GMu.Regularity]
E:12 [binder, in GMu.Regularity2]
E:12 [binder, in GMu.Regularity]
E:12 [binder, in GMu.CanonicalForms]
e:120 [binder, in GMu.Regularity]
e:120 [binder, in GMu.InfrastructureOpen]
E:122 [binder, in GMu.Preservation]
E:122 [binder, in GMu.InfrastructureFV]
e:124 [binder, in GMu.Preservation]
e:128 [binder, in GMu.InfrastructureOpen]
E:129 [binder, in GMu.Regularity]
E:13 [binder, in GMu.Preservation]
e:130 [binder, in GMu.Regularity]
e:130 [binder, in GMu.InfrastructureOpen]
e:132 [binder, in GMu.Definitions]
E:132 [binder, in GMu.Preservation]
E:132 [binder, in GMu.InfrastructureFV]
e:134 [binder, in GMu.Preservation]
E:135 [binder, in GMu.Regularity]
e:137 [binder, in GMu.Regularity]
e:139 [binder, in GMu.InfrastructureSubst]
e:142 [binder, in GMu.InfrastructureSubst]
E:142 [binder, in GMu.Preservation]
e:144 [binder, in GMu.Preservation]
e:147 [binder, in GMu.InfrastructureSubst]
e:148 [binder, in GMu.Definitions]
e:152 [binder, in GMu.InfrastructureSubst]
e:154 [binder, in GMu.Definitions]
E:158 [binder, in GMu.Preservation]
e:16 [binder, in GMu.Prelude]
e:164 [binder, in GMu.InfrastructureSubst]
e:164 [binder, in GMu.Preservation]
e:167 [binder, in GMu.Definitions]
E:168 [binder, in GMu.InfrastructureSubst]
E:169 [binder, in GMu.Preservation]
E:17 [binder, in GMu.Regularity2]
e:17 [binder, in GMu.Prelude]
e:174 [binder, in GMu.Preservation]
E:175 [binder, in GMu.InfrastructureSubst]
E:180 [binder, in GMu.Preservation]
e:181 [binder, in GMu.Preservation]
e:182 [binder, in GMu.Prelude]
E:188 [binder, in GMu.Preservation]
e:189 [binder, in GMu.Preservation]
e:19 [binder, in GMu.Prelude]
E:19 [binder, in GMu.Preservation]
E:2 [binder, in GMu.Regularity]
e:2 [binder, in GMu.Tests]
e:21 [binder, in GMu.Prelude]
e:21 [binder, in GMu.CanonicalForms]
e:22 [binder, in GMu.InfrastructureFV]
E:223 [binder, in GMu.SubstMatch]
E:23 [binder, in GMu.Regularity2]
e:23 [binder, in GMu.Prelude]
e:255 [binder, in GMu.Definitions]
e:26 [binder, in GMu.Prelude]
e:261 [binder, in GMu.Definitions]
e:27 [binder, in GMu.Prelude]
e:28 [binder, in GMu.Prelude]
e:28 [binder, in GMu.CanonicalForms]
E:28 [binder, in GMu.Preservation]
E:293 [binder, in GMu.Definitions]
E:3 [binder, in GMu.Regularity2]
E:3 [binder, in GMu.CanonicalForms]
E:30 [binder, in GMu.Regularity2]
e:31 [binder, in GMu.Prelude]
e:32 [binder, in GMu.Prelude]
e:34 [binder, in GMu.Prelude]
e:34 [binder, in GMu.CanonicalForms]
e:36 [binder, in GMu.Prelude]
E:37 [binder, in GMu.Preservation]
E:376 [binder, in GMu.Definitions]
e:38 [binder, in GMu.Prelude]
e:39 [binder, in GMu.CanonicalForms]
E:390 [binder, in GMu.Definitions]
E:392 [binder, in GMu.Definitions]
E:398 [binder, in GMu.Definitions]
e:40 [binder, in GMu.Definitions]
e:40 [binder, in GMu.Preservation]
E:41 [binder, in GMu.Regularity]
E:416 [binder, in GMu.Definitions]
e:42 [binder, in GMu.CanonicalForms]
E:424 [binder, in GMu.Definitions]
E:434 [binder, in GMu.Definitions]
E:44 [binder, in GMu.Regularity]
E:442 [binder, in GMu.Definitions]
E:450 [binder, in GMu.Definitions]
E:459 [binder, in GMu.Definitions]
E:466 [binder, in GMu.Definitions]
E:47 [binder, in GMu.Preservation]
E:474 [binder, in GMu.Definitions]
E:48 [binder, in GMu.Regularity2]
e:48 [binder, in GMu.InfrastructureFV]
E:483 [binder, in GMu.Definitions]
E:494 [binder, in GMu.Definitions]
e:495 [binder, in GMu.Definitions]
E:5 [binder, in GMu.Preservation]
e:5 [binder, in GMu.InfrastructureOpen]
E:50 [binder, in GMu.Regularity]
e:50 [binder, in GMu.InfrastructureSubst]
e:50 [binder, in GMu.InfrastructureFV]
e:51 [binder, in GMu.Definitions]
e:51 [binder, in GMu.InfrastructureSubst]
e:51 [binder, in GMu.InfrastructureOpen]
E:513 [binder, in GMu.Definitions]
e:516 [binder, in GMu.Definitions]
e:52 [binder, in GMu.Preservation]
E:53 [binder, in GMu.Equations]
e:53 [binder, in GMu.InfrastructureOpen]
E:54 [binder, in GMu.Regularity2]
e:54 [binder, in GMu.Equations]
e:550 [binder, in GMu.Definitions]
e:558 [binder, in GMu.Definitions]
E:56 [binder, in GMu.Regularity]
e:560 [binder, in GMu.Definitions]
e:58 [binder, in GMu.InfrastructureSubst]
e:58 [binder, in GMu.InfrastructureOpen]
e:585 [binder, in GMu.Definitions]
e:59 [binder, in GMu.Definitions]
e:590 [binder, in GMu.Definitions]
E:6 [binder, in GMu.Regularity]
E:60 [binder, in GMu.Equations]
e:61 [binder, in GMu.Equations]
e:61 [binder, in GMu.Definitions]
e:61 [binder, in GMu.InfrastructureSubst]
E:64 [binder, in GMu.Regularity]
e:64 [binder, in GMu.Definitions]
e:64 [binder, in GMu.InfrastructureOpen]
e:65 [binder, in GMu.InfrastructureSubst]
e:66 [binder, in GMu.InfrastructureOpen]
E:67 [binder, in GMu.Regularity2]
E:68 [binder, in GMu.Regularity]
e:69 [binder, in GMu.Definitions]
e:69 [binder, in GMu.InfrastructureOpen]
e:7 [binder, in GMu.InfrastructureFV]
e:71 [binder, in GMu.Definitions]
E:72 [binder, in GMu.Regularity2]
e:74 [binder, in GMu.Definitions]
e:75 [binder, in GMu.InfrastructureFV]
e:76 [binder, in GMu.InfrastructureSubst]
e:77 [binder, in GMu.InfrastructureOpen]
e:79 [binder, in GMu.Definitions]
E:8 [binder, in GMu.Regularity2]
e:80 [binder, in GMu.InfrastructureSubst]
e:80 [binder, in GMu.InfrastructureOpen]
e:80 [binder, in GMu.InfrastructureFV]
E:81 [binder, in GMu.Regularity2]
E:83 [binder, in GMu.InfrastructureFV]
e:84 [binder, in GMu.InfrastructureOpen]
e:85 [binder, in GMu.InfrastructureSubst]
E:87 [binder, in GMu.InfrastructureFV]
e:88 [binder, in GMu.InfrastructureOpen]
e:89 [binder, in GMu.InfrastructureSubst]
E:96 [binder, in GMu.Preservation]
e:96 [binder, in GMu.InfrastructureOpen]
e:97 [binder, in GMu.InfrastructureOpen]

F

fix_var [constructor, in GMu.Definitions]
fold_left_subset [lemma, in GMu.InfrastructureFV]
fold_left_subset_base [lemma, in GMu.InfrastructureFV]
fold_empty [lemma, in GMu.InfrastructureFV]
forall2_from_snd_zip [lemma, in GMu.Zip]
forall2_from_snd [lemma, in GMu.Zip]
Forall2_eq_len [lemma, in GMu.Prelude]
Forall2_eq [lemma, in GMu.TestCommon]
four [definition, in GMu.Tests2]
from_list_spec2 [lemma, in GMu.Prelude]
from_list_spec [lemma, in GMu.Prelude]
fst_from_zip [lemma, in GMu.Zip]
fv_env [definition, in GMu.Definitions]
fv_delta [definition, in GMu.Definitions]
fv_trm [definition, in GMu.Definitions]
fv_typs_migration [lemma, in GMu.Definitions]
fv_typs [definition, in GMu.Definitions]
fv_typ [definition, in GMu.Definitions]
fv_delta_equations [lemma, in GMu.InfrastructureFV]
fv_delta_alphas [lemma, in GMu.InfrastructureFV]
fv_delta_app [lemma, in GMu.InfrastructureFV]
fv_env_subst [lemma, in GMu.InfrastructureFV]
fv_subst_tt [lemma, in GMu.InfrastructureFV]
fv_env_extend [lemma, in GMu.InfrastructureFV]
fv_open_te_many [lemma, in GMu.InfrastructureFV]
fv_open_te [lemma, in GMu.InfrastructureFV]
fv_open_tt [lemma, in GMu.InfrastructureFV]
fv_smaller_many [lemma, in GMu.InfrastructureFV]
fv_typs_notin [lemma, in GMu.InfrastructureFV]
fv_smaller [lemma, in GMu.InfrastructureFV]
fv_open [lemma, in GMu.InfrastructureFV]
fv_fold_in [lemma, in GMu.InfrastructureFV]
fv_fold_in_clause [lemma, in GMu.InfrastructureFV]
fv_fold_in_general [lemma, in GMu.InfrastructureFV]
fv_fold_base_clause [lemma, in GMu.InfrastructureFV]
fv_fold_base [lemma, in GMu.InfrastructureFV]
fv_fold_general [lemma, in GMu.InfrastructureFV]
fv:100 [binder, in GMu.InfrastructureFV]
fv:108 [binder, in GMu.InfrastructureFV]
fv:11 [binder, in GMu.InfrastructureFV]
fv:135 [binder, in GMu.InfrastructureFV]
fv:158 [binder, in GMu.Definitions]
fv:16 [binder, in GMu.InfrastructureFV]
fv:164 [binder, in GMu.InfrastructureFV]
fv:165 [binder, in GMu.Definitions]
fv:170 [binder, in GMu.Definitions]
fv:171 [binder, in GMu.InfrastructureFV]
fv:172 [binder, in GMu.Definitions]
fv:26 [binder, in GMu.InfrastructureFV]
fv:32 [binder, in GMu.InfrastructureFV]
fv:40 [binder, in GMu.InfrastructureFV]
fv:49 [binder, in GMu.InfrastructureFV]
fv:6 [binder, in GMu.InfrastructureFV]
F0:107 [binder, in GMu.Preservation]
F0:113 [binder, in GMu.Preservation]
F0:19 [binder, in GMu.Regularity]
F0:21 [binder, in GMu.Regularity]
F0:58 [binder, in GMu.Preservation]
F0:64 [binder, in GMu.Preservation]
F0:70 [binder, in GMu.Preservation]
F0:76 [binder, in GMu.Preservation]
F0:84 [binder, in GMu.Preservation]
F0:90 [binder, in GMu.Preservation]
F1:95 [binder, in GMu.Equations]
F2_from_zip [lemma, in GMu.Zip]
F2_iff_In_zip [lemma, in GMu.Zip]
F2:96 [binder, in GMu.Equations]
f:10 [binder, in GMu.Zip]
f:103 [binder, in GMu.Prelude]
f:105 [binder, in GMu.Definitions]
f:108 [binder, in GMu.Definitions]
f:115 [binder, in GMu.Prelude]
f:128 [binder, in GMu.Prelude]
F:136 [binder, in GMu.Prelude]
F:143 [binder, in GMu.Preservation]
F:159 [binder, in GMu.Preservation]
f:162 [binder, in GMu.Prelude]
f:17 [binder, in GMu.Zip]
F:178 [binder, in GMu.Prelude]
F:184 [binder, in GMu.Prelude]
f:21 [binder, in GMu.TestCommon]
F:38 [binder, in GMu.Preservation]
F:4 [binder, in GMu.Regularity2]
f:45 [binder, in GMu.Prelude]
F:48 [binder, in GMu.Preservation]
f:50 [binder, in GMu.Prelude]
F:55 [binder, in GMu.Regularity2]
F:60 [binder, in GMu.Regularity]
F:73 [binder, in GMu.Regularity2]
f:82 [binder, in GMu.Prelude]
F:94 [binder, in GMu.Equations]
F:97 [binder, in GMu.Preservation]
F:98 [binder, in GMu.Zip]

G

GADTConstructor [definition, in GMu.Definitions]
GADTConstructorDef [record, in GMu.Definitions]
GADTC:53 [binder, in GMu.Definitions]
GADTDef [record, in GMu.Definitions]
GADTEnv [definition, in GMu.Definitions]
GADTName [definition, in GMu.Definitions]
gadt_constructor_ok [lemma, in GMu.Regularity]
GS [definition, in GMu.TestVector]
GTs:133 [binder, in GMu.InfrastructureOpen]
GZ [definition, in GMu.TestVector]
g:104 [binder, in GMu.Prelude]
g:116 [binder, in GMu.Prelude]
G:224 [binder, in GMu.Definitions]
G:39 [binder, in GMu.Preservation]
g:51 [binder, in GMu.Prelude]
G:538 [binder, in GMu.Definitions]
G:572 [binder, in GMu.Definitions]
G:78 [binder, in GMu.Definitions]
G:79 [binder, in GMu.InfrastructureOpen]
g:83 [binder, in GMu.Prelude]

H

head_types [lemma, in GMu.TestVector]
head_typ [definition, in GMu.TestVector]
head_trm [definition, in GMu.TestVector]
head_proof:93 [binder, in GMu.Definitions]
helper_equations_commute [lemma, in GMu.Preservation]
h:105 [binder, in GMu.Prelude]
h:3 [binder, in GMu.Definitions]
h:8 [binder, in GMu.TestVector]

I

id [definition, in GMu.Tests]
id_app_evals [lemma, in GMu.Tests]
id_app_types [lemma, in GMu.Tests]
id_app [definition, in GMu.Tests]
id_typ [definition, in GMu.Tests]
Infrastructure [library]
InfrastructureFV [library]
InfrastructureOpen [library]
InfrastructureSubst [library]
InfrastructureSubstPrim [library]
inversion_eq_typ_gadt [lemma, in GMu.Equations]
inversion_eq_typ_all [lemma, in GMu.Equations]
inversion_eq_tuple [lemma, in GMu.Equations]
inversion_eq_arrow [lemma, in GMu.Equations]
inversion_typing_eq [lemma, in GMu.Equations]
Inzip_from_nth_error [lemma, in GMu.Zip]
Inzip_to_nth_error [lemma, in GMu.Zip]
inzip_map_clause_trm [lemma, in GMu.Prelude]
in_from_list [lemma, in GMu.Prelude]
in_fold_exists [lemma, in GMu.InfrastructureFV]
in_domΔ_eq [lemma, in GMu.InfrastructureFV]
is_var_defined_split [lemma, in GMu.SubstMatch]
is_var_defined_dom [lemma, in GMu.SubstMatch]
is_var_defined [definition, in GMu.Definitions]
is_var_defined_split [lemma, in GMu.TestCommon]
i:119 [binder, in GMu.InfrastructureOpen]
i:124 [binder, in GMu.InfrastructureOpen]
i:45 [binder, in GMu.InfrastructureOpen]
i:51 [binder, in GMu.Zip]
i:64 [binder, in GMu.Zip]
i:67 [binder, in GMu.Zip]
i:74 [binder, in GMu.Zip]
i:87 [binder, in GMu.Zip]
i:94 [binder, in GMu.Zip]
i:95 [binder, in GMu.Zip]

J

JMeq_from_eq [lemma, in GMu.Prelude]
j:116 [binder, in GMu.InfrastructureOpen]
j:121 [binder, in GMu.InfrastructureOpen]
J:15 [binder, in GMu.InfrastructureOpen]

K

k:105 [binder, in GMu.InfrastructureOpen]
k:108 [binder, in GMu.InfrastructureSubst]
k:108 [binder, in GMu.InfrastructureOpen]
k:111 [binder, in GMu.InfrastructureOpen]
k:114 [binder, in GMu.InfrastructureOpen]
k:115 [binder, in GMu.Definitions]
k:118 [binder, in GMu.InfrastructureSubst]
k:12 [binder, in GMu.Prelude]
k:120 [binder, in GMu.Definitions]
k:122 [binder, in GMu.InfrastructureSubst]
k:123 [binder, in GMu.Definitions]
k:126 [binder, in GMu.InfrastructureOpen]
k:130 [binder, in GMu.Definitions]
k:131 [binder, in GMu.InfrastructureOpen]
k:16 [binder, in GMu.InfrastructureOpen]
k:18 [binder, in GMu.InfrastructureOpen]
k:19 [binder, in GMu.InfrastructureOpen]
k:22 [binder, in GMu.InfrastructureOpen]
k:25 [binder, in GMu.InfrastructureOpen]
k:259 [binder, in GMu.Definitions]
k:27 [binder, in GMu.InfrastructureOpen]
k:30 [binder, in GMu.InfrastructureOpen]
k:33 [binder, in GMu.InfrastructureOpen]
k:39 [binder, in GMu.InfrastructureOpen]
k:42 [binder, in GMu.InfrastructureOpen]
k:46 [binder, in GMu.InfrastructureOpen]
k:48 [binder, in GMu.Definitions]
k:49 [binder, in GMu.InfrastructureOpen]
k:50 [binder, in GMu.InfrastructureOpen]
k:52 [binder, in GMu.InfrastructureOpen]
k:53 [binder, in GMu.InfrastructureFV]
k:54 [binder, in GMu.InfrastructureOpen]
k:56 [binder, in GMu.InfrastructureFV]
k:57 [binder, in GMu.InfrastructureOpen]
k:59 [binder, in GMu.InfrastructureFV]
k:60 [binder, in GMu.InfrastructureOpen]
k:62 [binder, in GMu.InfrastructureFV]
k:63 [binder, in GMu.InfrastructureSubst]
k:63 [binder, in GMu.InfrastructureOpen]
k:65 [binder, in GMu.InfrastructureOpen]
k:68 [binder, in GMu.InfrastructureOpen]
k:69 [binder, in GMu.InfrastructureSubst]
k:71 [binder, in GMu.InfrastructureOpen]
k:74 [binder, in GMu.InfrastructureSubst]
k:74 [binder, in GMu.InfrastructureOpen]
k:74 [binder, in GMu.InfrastructureFV]
k:76 [binder, in GMu.InfrastructureFV]
k:78 [binder, in GMu.InfrastructureOpen]
k:82 [binder, in GMu.InfrastructureOpen]
k:86 [binder, in GMu.InfrastructureOpen]
k:87 [binder, in GMu.InfrastructureSubst]
k:91 [binder, in GMu.InfrastructureOpen]

L

lam_var [constructor, in GMu.Definitions]
la:11 [binder, in GMu.Zip]
la:163 [binder, in GMu.Prelude]
la:18 [binder, in GMu.Zip]
la:23 [binder, in GMu.Zip]
la:27 [binder, in GMu.Zip]
la:4 [binder, in GMu.Zip]
lb:12 [binder, in GMu.Zip]
lb:164 [binder, in GMu.Prelude]
lb:19 [binder, in GMu.Zip]
lb:24 [binder, in GMu.Zip]
lb:28 [binder, in GMu.Zip]
lb:5 [binder, in GMu.Zip]
length_equality [lemma, in GMu.Prelude]
len:74 [binder, in GMu.Prelude]
let_id_app_evals [lemma, in GMu.Tests]
let_id_app_types [lemma, in GMu.Tests]
let_id_app [definition, in GMu.Tests]
LibList_mem [lemma, in GMu.Prelude]
LibList_map [lemma, in GMu.Prelude]
lists_map_eq [lemma, in GMu.Prelude]
list_fold_map [lemma, in GMu.Prelude]
list_clause_ind:96 [binder, in GMu.Definitions]
list_typ_ind:31 [binder, in GMu.Definitions]
loop [definition, in GMu.Tests]
loop_type [lemma, in GMu.Tests]
LPt:30 [binder, in GMu.Definitions]
ls:105 [binder, in GMu.InfrastructureFV]
ls:114 [binder, in GMu.Prelude]
ls:14 [binder, in GMu.InfrastructureFV]
ls:21 [binder, in GMu.Definitions]
ls:24 [binder, in GMu.InfrastructureFV]
ls:26 [binder, in GMu.Definitions]
ls:3 [binder, in GMu.InfrastructureFV]
ls:30 [binder, in GMu.InfrastructureFV]
ls:38 [binder, in GMu.InfrastructureFV]
ls:44 [binder, in GMu.InfrastructureFV]
ls:46 [binder, in GMu.Prelude]
ls:59 [binder, in GMu.Prelude]
ls:9 [binder, in GMu.InfrastructureFV]
ls:98 [binder, in GMu.Definitions]
ls:99 [binder, in GMu.Zip]
l1:174 [binder, in GMu.Prelude]
l2:175 [binder, in GMu.Prelude]
L:12 [binder, in GMu.TestVector]
l:127 [binder, in GMu.Prelude]
L:131 [binder, in GMu.Prelude]
l:179 [binder, in GMu.Prelude]
L:181 [binder, in GMu.Definitions]
L:201 [binder, in GMu.Definitions]
L:207 [binder, in GMu.Definitions]
L:213 [binder, in GMu.Definitions]
L:218 [binder, in GMu.Definitions]
L:222 [binder, in GMu.Definitions]
L:311 [binder, in GMu.Definitions]
L:356 [binder, in GMu.Definitions]
L:360 [binder, in GMu.Definitions]
L:413 [binder, in GMu.Definitions]
L:431 [binder, in GMu.Definitions]
L:471 [binder, in GMu.Definitions]
L:480 [binder, in GMu.Definitions]
L:491 [binder, in GMu.Definitions]
l:52 [binder, in GMu.Prelude]
l:548 [binder, in GMu.Definitions]
L:69 [binder, in GMu.Prelude]
L:72 [binder, in GMu.Prelude]
L:73 [binder, in GMu.Prelude]
l:84 [binder, in GMu.Prelude]

M

ManyTest [section, in GMu.DefinitionsTests]
ManyTest.T [variable, in GMu.DefinitionsTests]
map [definition, in GMu.TestVector]
map_types [lemma, in GMu.TestVector]
map_map [lemma, in GMu.Prelude]
map_id [lemma, in GMu.Prelude]
map_clause_trm_trm [definition, in GMu.Definitions]
map_clause_trms [definition, in GMu.Definitions]
mkGADT [constructor, in GMu.Definitions]
mkGADTconstructor [constructor, in GMu.Definitions]
mk_type_equation [constructor, in GMu.Definitions]
ms:225 [binder, in GMu.Definitions]
ms:496 [binder, in GMu.Definitions]
ms:541 [binder, in GMu.Definitions]
ms:573 [binder, in GMu.Definitions]
ms:81 [binder, in GMu.InfrastructureOpen]
m:11 [binder, in GMu.Prelude]

N

Name:18 [binder, in GMu.CanonicalForms]
Name:185 [binder, in GMu.Definitions]
Name:194 [binder, in GMu.Definitions]
Name:237 [binder, in GMu.Definitions]
Name:319 [binder, in GMu.Definitions]
Name:366 [binder, in GMu.Definitions]
Name:402 [binder, in GMu.Definitions]
Name:499 [binder, in GMu.Definitions]
Name:5 [binder, in GMu.CanonicalForms]
Name:91 [binder, in GMu.Regularity]
Nat [axiom, in GMu.Tests2]
NatDef [definition, in GMu.Tests2]
natSigma [definition, in GMu.Tests2]
neq_from_notin [lemma, in GMu.TestCommon]
nil [definition, in GMu.TestVector]
Nil [definition, in GMu.TestVector]
nil_type [lemma, in GMu.TestVector]
Notations [library]
notin_eqv [lemma, in GMu.TestVector]
notin_fv_wf [lemma, in GMu.Regularity]
notin_from_list [lemma, in GMu.Equations]
notin_inverse [lemma, in GMu.Prelude]
notin_domDelta_subst_td [lemma, in GMu.InfrastructureFV]
notin_env_binds [lemma, in GMu.InfrastructureFV]
notin_dom_tc_vars [lemma, in GMu.InfrastructureFV]
notin_domΔ_eq [lemma, in GMu.InfrastructureFV]
notin_env_inv [lemma, in GMu.InfrastructureFV]
notin_fv_tt_open [lemma, in GMu.InfrastructureFV]
notin_fold [lemma, in GMu.InfrastructureFV]
nth_error_map [lemma, in GMu.Zip]
nth_error_zip_merge [lemma, in GMu.Zip]
nth_error_zip_split [lemma, in GMu.Zip]
nth_error_implies_zip_swap [lemma, in GMu.Zip]
nth_error_implies_zip [lemma, in GMu.Zip]
nth_error_map [lemma, in GMu.Prelude]
n:10 [binder, in GMu.InfrastructureOpen]
n:100 [binder, in GMu.InfrastructureOpen]
n:101 [binder, in GMu.InfrastructureOpen]
n:104 [binder, in GMu.InfrastructureOpen]
n:107 [binder, in GMu.InfrastructureOpen]
n:110 [binder, in GMu.InfrastructureOpen]
n:13 [binder, in GMu.Prelude]
N:134 [binder, in GMu.InfrastructureOpen]
n:15 [binder, in GMu.Prelude]
n:18 [binder, in GMu.Prelude]
n:180 [binder, in GMu.Prelude]
N:19 [binder, in GMu.InfrastructureSubstPrim]
n:20 [binder, in GMu.Prelude]
n:22 [binder, in GMu.Prelude]
n:22 [binder, in GMu.Definitions]
n:25 [binder, in GMu.Prelude]
N:29 [binder, in GMu.InfrastructureOpen]
n:3 [binder, in GMu.InfrastructureOpen]
n:30 [binder, in GMu.Prelude]
N:30 [binder, in GMu.TestCommon]
n:33 [binder, in GMu.Prelude]
n:34 [binder, in GMu.InfrastructureOpen]
n:35 [binder, in GMu.Prelude]
n:37 [binder, in GMu.Prelude]
n:38 [binder, in GMu.InfrastructureOpen]
n:40 [binder, in GMu.Prelude]
N:44 [binder, in GMu.CanonicalForms]
n:46 [binder, in GMu.Definitions]
N:7 [binder, in GMu.TestVector]
n:7 [binder, in GMu.InfrastructureOpen]
N:76 [binder, in GMu.InfrastructureOpen]
n:8 [binder, in GMu.Definitions]
n:8 [binder, in GMu.InfrastructureSubst]
n:87 [binder, in GMu.InfrastructureOpen]
N:91 [binder, in GMu.Equations]
n:92 [binder, in GMu.InfrastructureOpen]
N:94 [binder, in GMu.InfrastructureOpen]
n:95 [binder, in GMu.InfrastructureOpen]

O

okConstructorDef [inductive, in GMu.Definitions]
okGadt [definition, in GMu.Definitions]
oknat [lemma, in GMu.Tests2]
oksigma [lemma, in GMu.TestVector]
oksigma [lemma, in GMu.TestEquality]
okt [inductive, in GMu.Definitions]
okt_strengthen_delta_eq [lemma, in GMu.Regularity2]
okt_replace_typ [lemma, in GMu.Regularity2]
okt_through_subst_tdtb [lemma, in GMu.Regularity2]
okt_is_wft_2 [lemma, in GMu.Regularity2]
okt_push_fresh [lemma, in GMu.Regularity2]
okt_weakening_delta_many [lemma, in GMu.Regularity2]
okt_weakening_delta_many_eq [lemma, in GMu.Regularity2]
okt_weakening_delta_eq [lemma, in GMu.Regularity2]
okt_weakening_delta [lemma, in GMu.Regularity2]
okt_strengthen_simple [lemma, in GMu.Regularity2]
okt_is_type [lemma, in GMu.Regularity]
okt_strengthen_delta_var [lemma, in GMu.Regularity]
okt_strengthen [lemma, in GMu.Regularity]
okt_is_wft [lemma, in GMu.Regularity]
okt_push_var_inv [lemma, in GMu.Regularity]
okt_implies_okgadt [lemma, in GMu.Regularity]
okt_is_ok [lemma, in GMu.Regularity]
okt_typ [constructor, in GMu.Definitions]
okt_empty [constructor, in GMu.Definitions]
ok_constr_def [constructor, in GMu.Definitions]
one [definition, in GMu.Tests2]
one_type [lemma, in GMu.Tests2]
only_vars_is_tc_vars [lemma, in GMu.Equations]
opening_adds_one [lemma, in GMu.InfrastructureOpen]
open_te_many_test [lemma, in GMu.DefinitionsTests]
open_tt_many_test [lemma, in GMu.DefinitionsTests]
open_typlist_test [lemma, in GMu.DefinitionsTests]
open_ee_test [lemma, in GMu.DefinitionsTests]
open_te_test [lemma, in GMu.DefinitionsTests]
open_tt_test [lemma, in GMu.DefinitionsTests]
open_te_many_var [definition, in GMu.Definitions]
open_tt_many_var [definition, in GMu.Definitions]
open_te_many [definition, in GMu.Definitions]
open_tt_many [definition, in GMu.Definitions]
open_ee [definition, in GMu.Definitions]
open_te [definition, in GMu.Definitions]
open_tt [definition, in GMu.Definitions]
open_ee_rec [definition, in GMu.Definitions]
open_te_rec [definition, in GMu.Definitions]
open_typlist_rec [definition, in GMu.Definitions]
open_tt_rec [definition, in GMu.Definitions]
open_tt_many_closed [lemma, in GMu.InfrastructureOpen]
open_ee_rec_term [lemma, in GMu.InfrastructureOpen]
open_ee_rec_type_many [lemma, in GMu.InfrastructureOpen]
open_ee_rec_type_core [lemma, in GMu.InfrastructureOpen]
open_ee_rec_term_core [lemma, in GMu.InfrastructureOpen]
open_te_rec_term [lemma, in GMu.InfrastructureOpen]
open_tt_rec_type [lemma, in GMu.InfrastructureOpen]
open_tt_var_preserves_size [lemma, in GMu.InfrastructureOpen]
open_te_var_preserves_size [lemma, in GMu.InfrastructureOpen]
open_ee_var_preserves_size [lemma, in GMu.InfrastructureOpen]
OTs:132 [binder, in GMu.InfrastructureOpen]
O1:130 [binder, in GMu.SubstMatch]
O1:140 [binder, in GMu.SubstMatch]
O1:146 [binder, in GMu.SubstMatch]
O1:146 [binder, in GMu.InfrastructureFV]
O1:160 [binder, in GMu.SubstMatch]
O1:173 [binder, in GMu.SubstMatch]
O1:175 [binder, in GMu.InfrastructureFV]
O1:186 [binder, in GMu.SubstMatch]
O1:194 [binder, in GMu.SubstMatch]
O1:20 [binder, in GMu.SubstMatch]
O1:219 [binder, in GMu.SubstMatch]
O1:238 [binder, in GMu.SubstMatch]
O1:27 [binder, in GMu.SubstMatch]
O1:38 [binder, in GMu.SubstMatch]
O2:141 [binder, in GMu.SubstMatch]
O2:147 [binder, in GMu.SubstMatch]
O2:147 [binder, in GMu.InfrastructureFV]
O2:174 [binder, in GMu.SubstMatch]
O2:176 [binder, in GMu.InfrastructureFV]
O2:187 [binder, in GMu.SubstMatch]
O2:195 [binder, in GMu.SubstMatch]
O2:220 [binder, in GMu.SubstMatch]
O2:239 [binder, in GMu.SubstMatch]
O2:29 [binder, in GMu.SubstMatch]
O:103 [binder, in GMu.SubstMatch]
O:108 [binder, in GMu.SubstMatch]
O:11 [binder, in GMu.InfrastructureSubstPrim]
O:114 [binder, in GMu.SubstMatch]
O:119 [binder, in GMu.SubstMatch]
O:123 [binder, in GMu.SubstMatch]
O:14 [binder, in GMu.InfrastructureSubstPrim]
O:143 [binder, in GMu.InfrastructureFV]
O:148 [binder, in GMu.InfrastructureFV]
O:17 [binder, in GMu.InfrastructureSubstPrim]
O:178 [binder, in GMu.InfrastructureFV]
O:181 [binder, in GMu.SubstMatch]
O:193 [binder, in GMu.SubstMatch]
O:21 [binder, in GMu.InfrastructureSubstPrim]
O:22 [binder, in GMu.InfrastructureSubstPrim]
O:231 [binder, in GMu.SubstMatch]
O:86 [binder, in GMu.SubstMatch]
O:9 [binder, in GMu.InfrastructureSubstPrim]
O:93 [binder, in GMu.SubstMatch]
O:97 [binder, in GMu.SubstMatch]

P

Ph:134 [binder, in GMu.Prelude]
plus [definition, in GMu.Tests2]
plus_evals4 [lemma, in GMu.Tests2]
plus_evals [lemma, in GMu.Tests2]
plus_types [lemma, in GMu.Tests2]
Prelude [library]
preservation [definition, in GMu.Definitions]
Preservation [library]
preservation_thm [lemma, in GMu.Preservation]
preservation_evals [lemma, in GMu.Tests]
progress [definition, in GMu.Definitions]
Progress [library]
progress_thm [lemma, in GMu.Progress]
Ps:146 [binder, in GMu.Preservation]
Ps:173 [binder, in GMu.InfrastructureSubst]
Ps:177 [binder, in GMu.InfrastructureSubst]
Ps:273 [binder, in GMu.Definitions]
Pts:135 [binder, in GMu.Prelude]
Pt:29 [binder, in GMu.Definitions]
P:10 [binder, in GMu.Prelude]
P:104 [binder, in GMu.InfrastructureFV]
P:106 [binder, in GMu.SubstMatch]
P:111 [binder, in GMu.SubstMatch]
P:111 [binder, in GMu.InfrastructureSubst]
P:113 [binder, in GMu.InfrastructureFV]
P:114 [binder, in GMu.InfrastructureSubst]
P:117 [binder, in GMu.InfrastructureFV]
P:12 [binder, in GMu.InfrastructureSubst]
P:125 [binder, in GMu.InfrastructureSubst]
P:125 [binder, in GMu.Preservation]
P:129 [binder, in GMu.InfrastructureSubst]
P:130 [binder, in GMu.InfrastructureFV]
P:135 [binder, in GMu.InfrastructureSubst]
P:135 [binder, in GMu.Preservation]
P:14 [binder, in GMu.Prelude]
P:148 [binder, in GMu.Preservation]
P:154 [binder, in GMu.Preservation]
P:161 [binder, in GMu.InfrastructureFV]
P:168 [binder, in GMu.InfrastructureFV]
P:170 [binder, in GMu.InfrastructureSubst]
P:173 [binder, in GMu.Prelude]
P:180 [binder, in GMu.InfrastructureFV]
P:182 [binder, in GMu.InfrastructureSubst]
P:184 [binder, in GMu.InfrastructureFV]
P:188 [binder, in GMu.InfrastructureFV]
p:20 [binder, in GMu.Zip]
P:200 [binder, in GMu.SubstMatch]
P:23 [binder, in GMu.InfrastructureFV]
P:24 [binder, in GMu.Prelude]
P:26 [binder, in GMu.InfrastructureSubstPrim]
P:265 [binder, in GMu.Definitions]
P:29 [binder, in GMu.Prelude]
p:294 [binder, in GMu.Definitions]
P:33 [binder, in GMu.Zip]
P:33 [binder, in GMu.InfrastructureSubst]
P:38 [binder, in GMu.Regularity2]
P:39 [binder, in GMu.Prelude]
P:39 [binder, in GMu.InfrastructureSubst]
P:4 [binder, in GMu.InfrastructureFV]
P:40 [binder, in GMu.Zip]
P:44 [binder, in GMu.Regularity2]
P:47 [binder, in GMu.InfrastructureFV]
P:5 [binder, in GMu.InfrastructureSubstPrim]
P:60 [binder, in GMu.Regularity2]
P:60 [binder, in GMu.Prelude]
P:69 [binder, in GMu.Regularity2]
P:7 [binder, in GMu.InfrastructureSubst]
P:82 [binder, in GMu.InfrastructureSubst]
P:84 [binder, in GMu.Regularity]
P:93 [binder, in GMu.InfrastructureSubst]
P:98 [binder, in GMu.InfrastructureSubst]

R

red [inductive, in GMu.Definitions]
red_match [constructor, in GMu.Definitions]
red_fix [constructor, in GMu.Definitions]
red_snd [constructor, in GMu.Definitions]
red_fst [constructor, in GMu.Definitions]
red_letbeta [constructor, in GMu.Definitions]
red_tbeta [constructor, in GMu.Definitions]
red_beta [constructor, in GMu.Definitions]
Refl [definition, in GMu.TestEquality]
Regularity [library]
Regularity2 [library]
remove_true_equations [lemma, in GMu.Preservation]
remove_true_equation [lemma, in GMu.Preservation]
retTs:354 [binder, in GMu.Definitions]
retT:363 [binder, in GMu.Definitions]
rewrite_open_tt_many_gadt [lemma, in GMu.InfrastructureOpen]
rT:364 [binder, in GMu.Definitions]

S

sigma [definition, in GMu.TestVector]
sigma [definition, in GMu.TestEquality]
SimpleEquationProperties [section, in GMu.Equations]
SimpleEquationProperties.Σ [variable, in GMu.Equations]
snd_from_zip [lemma, in GMu.Zip]
sources_distinct [lemma, in GMu.SubstMatch]
sources_list_fst [lemma, in GMu.InfrastructureFV]
spawn_unit_subst [lemma, in GMu.Equations]
split_notin_subset_union [lemma, in GMu.Prelude]
strong_induction_on_typ_size [lemma, in GMu.Prelude]
strong_induction_on_type_size_helper [lemma, in GMu.Prelude]
strong_induction_on_term_size [lemma, in GMu.Prelude]
strong_induction_on_term_size_helper [lemma, in GMu.Prelude]
strong_induction [lemma, in GMu.Prelude]
sublist_head_prop [lemma, in GMu.InfrastructureSubst]
sublist_tail_prop [lemma, in GMu.InfrastructureSubst]
subset_transitive [lemma, in GMu.Prelude]
subset_fold [lemma, in GMu.InfrastructureFV]
substitution [definition, in GMu.Definitions]
substitution_sources [definition, in GMu.Definitions]
substitution_sources_from_in [lemma, in GMu.InfrastructureFV]
SubstMatch [library]
subst_td_eqs [lemma, in GMu.Regularity2]
subst_strengthen_true_eq [lemma, in GMu.SubstMatch]
subst_match_inv_missing_var [lemma, in GMu.SubstMatch]
subst_eq_weaken2 [lemma, in GMu.SubstMatch]
subst_match_split [lemma, in GMu.SubstMatch]
subst_remove_used_var [lemma, in GMu.SubstMatch]
subst_eq_reorder2 [lemma, in GMu.SubstMatch]
subst_eq_reorder2_2 [lemma, in GMu.SubstMatch]
subst_eq_reorder1 [lemma, in GMu.SubstMatch]
subst_tt_split [lemma, in GMu.SubstMatch]
subst_eq_reorder1_2 [lemma, in GMu.SubstMatch]
subst_idempotent_simple [lemma, in GMu.SubstMatch]
subst_has_closed [lemma, in GMu.SubstMatch]
subst_has_wft [lemma, in GMu.SubstMatch]
subst_tt_prime_reduce_typ_fvar_undefined [lemma, in GMu.SubstMatch]
subst_tt_prime_reduce_typ_fvar_defined [lemma, in GMu.SubstMatch]
subst_match_remove_right_var3 [lemma, in GMu.SubstMatch]
subst_match_remove_unused_var [lemma, in GMu.SubstMatch]
subst_eq_weaken [lemma, in GMu.SubstMatch]
subst_eq_strengthen_gen [lemma, in GMu.SubstMatch]
subst_eq_strengthen [lemma, in GMu.SubstMatch]
subst_match_remove_right_var2 [lemma, in GMu.SubstMatch]
subst_match_remove_right_var [lemma, in GMu.SubstMatch]
subst_match_notin_srcs [lemma, in GMu.SubstMatch]
subst_match_decompose_var [lemma, in GMu.SubstMatch]
subst_match_remove_eq [lemma, in GMu.SubstMatch]
subst_sources_from_match [lemma, in GMu.SubstMatch]
subst_has_no_fv2 [lemma, in GMu.Equations]
subst_ttΘ_into_tuple [lemma, in GMu.Equations]
subst_ttΘ_into_abs [lemma, in GMu.Equations]
subst_has_no_fv [lemma, in GMu.Equations]
subst_tb_many_split [lemma, in GMu.Prelude]
subst_td_many [definition, in GMu.Definitions]
subst_td [definition, in GMu.Definitions]
subst_matches_typctx [inductive, in GMu.Definitions]
subst_tt' [definition, in GMu.Definitions]
subst_tb_many [definition, in GMu.Definitions]
subst_tt_many [definition, in GMu.Definitions]
subst_tb [definition, in GMu.Definitions]
subst_ee [definition, in GMu.Definitions]
subst_te [definition, in GMu.Definitions]
subst_tt [definition, in GMu.Definitions]
subst_ee_fix_value [lemma, in GMu.InfrastructureSubst]
subst_ee_fix_term [lemma, in GMu.InfrastructureSubst]
subst_commute [lemma, in GMu.InfrastructureSubst]
subst_tb_many_id_on_fresh_env [lemma, in GMu.InfrastructureSubst]
subst_tt_many_id_on_fresh [lemma, in GMu.InfrastructureSubst]
subst_tb_id_on_fresh [lemma, in GMu.InfrastructureSubst]
subst_te_many_commutes_open [lemma, in GMu.InfrastructureSubst]
subst_tt_many_free [lemma, in GMu.InfrastructureSubst]
subst_te_intro_many [lemma, in GMu.InfrastructureSubst]
subst_intro_commutes_opens_te [lemma, in GMu.InfrastructureSubst]
subst_commutes_with_unrelated_opens_te [lemma, in GMu.InfrastructureSubst]
subst_te_many [definition, in GMu.InfrastructureSubst]
subst_commutes_open_tt_many [lemma, in GMu.InfrastructureSubst]
subst_removes_var [lemma, in GMu.InfrastructureSubst]
subst_idempotent_through_many_open [lemma, in GMu.InfrastructureSubst]
subst_idempotent [lemma, in GMu.InfrastructureSubst]
subst_ee_value [lemma, in GMu.InfrastructureSubst]
subst_ee_term [lemma, in GMu.InfrastructureSubst]
subst_te_value [lemma, in GMu.InfrastructureSubst]
subst_te_term [lemma, in GMu.InfrastructureSubst]
subst_commutes_with_unrelated_opens_te_ee [lemma, in GMu.InfrastructureSubst]
subst_commutes_with_unrelated_opens_te_te [lemma, in GMu.InfrastructureSubst]
subst_tt_type [lemma, in GMu.InfrastructureSubst]
subst_map_reverse_type [lemma, in GMu.InfrastructureSubst]
subst_ee_open_te_var [lemma, in GMu.InfrastructureSubst]
subst_te_open_ee_var [lemma, in GMu.InfrastructureSubst]
subst_ee_intro [lemma, in GMu.InfrastructureSubst]
subst_ee_open_ee_var [lemma, in GMu.InfrastructureSubst]
subst_ee_open_ee [lemma, in GMu.InfrastructureSubst]
subst_ee_fresh [lemma, in GMu.InfrastructureSubst]
subst_te_intro [lemma, in GMu.InfrastructureSubst]
subst_te_open_te_var [lemma, in GMu.InfrastructureSubst]
subst_te_open_te [lemma, in GMu.InfrastructureSubst]
subst_te_fresh [lemma, in GMu.InfrastructureSubst]
subst_tt_intro_many [lemma, in GMu.InfrastructureSubst]
subst_intro_commutes_opens [lemma, in GMu.InfrastructureSubst]
subst_commutes_with_unrelated_opens [lemma, in GMu.InfrastructureSubst]
subst_tt_intro [lemma, in GMu.InfrastructureSubst]
subst_tt_open_tt_var [lemma, in GMu.InfrastructureSubst]
subst_tt_open_tt [lemma, in GMu.InfrastructureSubst]
subst_tt_open_tt_rec [lemma, in GMu.InfrastructureSubst]
subst_tt_fresh [lemma, in GMu.InfrastructureSubst]
subst_td_alphas [lemma, in GMu.InfrastructureFV]
subst_src_app [lemma, in GMu.InfrastructureFV]
subst_match_notin_srcs2 [lemma, in GMu.InfrastructureFV]
subst_ttprim_open_tt [lemma, in GMu.InfrastructureSubstPrim]
subst_tt_prime_reduce_typ_unit [lemma, in GMu.InfrastructureSubstPrim]
subst_tt_prime_reduce_typ_gadt [lemma, in GMu.InfrastructureSubstPrim]
subst_tt_prime_reduce_arrow [lemma, in GMu.InfrastructureSubstPrim]
subst_tt_prime_reduce_tuple [lemma, in GMu.InfrastructureSubstPrim]
subst_tt_prime_reduce_typ_all [lemma, in GMu.InfrastructureSubstPrim]
subst_tt_inside [lemma, in GMu.InfrastructureSubstPrim]
subst_ttΘ_fresh [lemma, in GMu.InfrastructureSubstPrim]
Succ [axiom, in GMu.TestVector]
succ [definition, in GMu.Tests2]
succ_type [lemma, in GMu.Tests2]
sum [definition, in GMu.Definitions]
symmetry_types [lemma, in GMu.TestEquality]
symmetry_trm [definition, in GMu.TestEquality]
symmetry_typ [definition, in GMu.TestEquality]

T

tail_proof:95 [binder, in GMu.Definitions]
Targ:410 [binder, in GMu.Definitions]
Tarity [projection, in GMu.Definitions]
Tarity:350 [binder, in GMu.Definitions]
Tarity:405 [binder, in GMu.Definitions]
Tarity:501 [binder, in GMu.Definitions]
Tarity:92 [binder, in GMu.Regularity]
TA1:73 [binder, in GMu.Equations]
TA1:79 [binder, in GMu.Equations]
TA2:75 [binder, in GMu.Equations]
TA2:81 [binder, in GMu.Equations]
TB1:74 [binder, in GMu.Equations]
TB1:80 [binder, in GMu.Equations]
TB2:76 [binder, in GMu.Equations]
TB2:82 [binder, in GMu.Equations]
Tconstructors [projection, in GMu.Definitions]
tc_vars [definition, in GMu.Definitions]
tc_add_eq [constructor, in GMu.Definitions]
tc_add_var [constructor, in GMu.Definitions]
tc_empty [constructor, in GMu.Definitions]
tc_eq [constructor, in GMu.Definitions]
tc_var [constructor, in GMu.Definitions]
tc:33 [binder, in GMu.Equations]
Tc:500 [binder, in GMu.Definitions]
teq_open [lemma, in GMu.SubstMatch]
teq_axiom [lemma, in GMu.Equations]
teq_transitivity [lemma, in GMu.Equations]
teq_symmetry [lemma, in GMu.Equations]
teq_reflexivity [lemma, in GMu.Equations]
term [inductive, in GMu.Definitions]
term_matchgadt [constructor, in GMu.Definitions]
term_let [constructor, in GMu.Definitions]
term_fix [constructor, in GMu.Definitions]
term_tapp [constructor, in GMu.Definitions]
term_tabs [constructor, in GMu.Definitions]
term_app [constructor, in GMu.Definitions]
term_abs [constructor, in GMu.Definitions]
term_snd [constructor, in GMu.Definitions]
term_fst [constructor, in GMu.Definitions]
term_tuple [constructor, in GMu.Definitions]
term_unit [constructor, in GMu.Definitions]
term_constructor [constructor, in GMu.Definitions]
term_var [constructor, in GMu.Definitions]
term_te_closed [lemma, in GMu.InfrastructureOpen]
TestCommon [library]
TestEquality [library]
Tests [library]
Tests2 [library]
TestVector [library]
te_closed_id [lemma, in GMu.InfrastructureOpen]
te_opening_te_many_adds [lemma, in GMu.InfrastructureOpen]
te_opening_ee_preserves [lemma, in GMu.InfrastructureOpen]
te_opening_te_adds_one [lemma, in GMu.InfrastructureOpen]
te_closed_in_surroundings [inductive, in GMu.InfrastructureOpen]
Tgen [constructor, in GMu.Definitions]
Tgen_from_any [lemma, in GMu.Regularity]
Tparams:13 [binder, in GMu.CanonicalForms]
Tparams:184 [binder, in GMu.Definitions]
Tparams:193 [binder, in GMu.Definitions]
Tparams:236 [binder, in GMu.Definitions]
Tparams:318 [binder, in GMu.Definitions]
Tparams:4 [binder, in GMu.CanonicalForms]
Tparams:91 [binder, in GMu.InfrastructureSubst]
Tparam:186 [binder, in GMu.Definitions]
Tparam:196 [binder, in GMu.Definitions]
Tparam:94 [binder, in GMu.InfrastructureSubst]
Tparam:95 [binder, in GMu.InfrastructureSubst]
transitivity_types [lemma, in GMu.TestEquality]
transitivity_trm [definition, in GMu.TestEquality]
transitivity_typ [definition, in GMu.TestEquality]
Treg [constructor, in GMu.Definitions]
Tret:411 [binder, in GMu.Definitions]
trm [inductive, in GMu.Definitions]
trm_size [definition, in GMu.Definitions]
trm_ind' [definition, in GMu.Definitions]
trm_ind'.trm_let_case [variable, in GMu.Definitions]
trm_ind'.trm_match_case [variable, in GMu.Definitions]
trm_ind'.trm_fix_case [variable, in GMu.Definitions]
trm_ind'.trm_tapp_case [variable, in GMu.Definitions]
trm_ind'.trm_tabs_case [variable, in GMu.Definitions]
trm_ind'.trm_app_case [variable, in GMu.Definitions]
trm_ind'.trm_abs_case [variable, in GMu.Definitions]
trm_ind'.trm_snd_case [variable, in GMu.Definitions]
trm_ind'.trm_fst_case [variable, in GMu.Definitions]
trm_ind'.trm_tuple_case [variable, in GMu.Definitions]
trm_ind'.trm_unit_case [variable, in GMu.Definitions]
trm_ind'.trm_constructor_case [variable, in GMu.Definitions]
trm_ind'.trm_fvar_case [variable, in GMu.Definitions]
trm_ind'.trm_bvar_case [variable, in GMu.Definitions]
trm_ind'.P [variable, in GMu.Definitions]
trm_ind' [section, in GMu.Definitions]
trm_let [constructor, in GMu.Definitions]
trm_matchgadt [constructor, in GMu.Definitions]
trm_fix [constructor, in GMu.Definitions]
trm_tapp [constructor, in GMu.Definitions]
trm_tabs [constructor, in GMu.Definitions]
trm_app [constructor, in GMu.Definitions]
trm_abs [constructor, in GMu.Definitions]
trm_snd [constructor, in GMu.Definitions]
trm_fst [constructor, in GMu.Definitions]
trm_tuple [constructor, in GMu.Definitions]
trm_unit [constructor, in GMu.Definitions]
trm_constructor [constructor, in GMu.Definitions]
trm_fvar [constructor, in GMu.Definitions]
trm_bvar [constructor, in GMu.Definitions]
Ts':45 [binder, in GMu.CanonicalForms]
Ts:107 [binder, in GMu.Regularity]
ts:122 [binder, in GMu.Definitions]
Ts:133 [binder, in GMu.InfrastructureSubst]
Ts:155 [binder, in GMu.InfrastructureFV]
Ts:159 [binder, in GMu.InfrastructureSubst]
Ts:160 [binder, in GMu.Definitions]
Ts:163 [binder, in GMu.Definitions]
Ts:163 [binder, in GMu.InfrastructureSubst]
Ts:168 [binder, in GMu.Prelude]
Ts:18 [binder, in GMu.InfrastructureSubstPrim]
Ts:192 [binder, in GMu.Preservation]
Ts:196 [binder, in GMu.Preservation]
Ts:210 [binder, in GMu.SubstMatch]
Ts:22 [binder, in GMu.TestCommon]
Ts:28 [binder, in GMu.InfrastructureOpen]
Ts:28 [binder, in GMu.TestCommon]
Ts:380 [binder, in GMu.Definitions]
Ts:401 [binder, in GMu.Definitions]
Ts:43 [binder, in GMu.CanonicalForms]
Ts:497 [binder, in GMu.Definitions]
Ts:52 [binder, in GMu.Definitions]
Ts:540 [binder, in GMu.Definitions]
Ts:61 [binder, in GMu.Regularity2]
Ts:63 [binder, in GMu.InfrastructureFV]
Ts:75 [binder, in GMu.InfrastructureOpen]
Ts:79 [binder, in GMu.InfrastructureFV]
Ts:89 [binder, in GMu.Equations]
Ts:97 [binder, in GMu.Equations]
Ts:98 [binder, in GMu.InfrastructureFV]
Tts:126 [binder, in GMu.InfrastructureSubst]
TT1:103 [binder, in GMu.Preservation]
TT1:400 [binder, in GMu.Definitions]
TT1:429 [binder, in GMu.Definitions]
TT1:455 [binder, in GMu.Definitions]
TT1:488 [binder, in GMu.Definitions]
TT1:503 [binder, in GMu.Definitions]
TT1:54 [binder, in GMu.Preservation]
TT2:104 [binder, in GMu.Preservation]
TT2:430 [binder, in GMu.Definitions]
TT2:456 [binder, in GMu.Definitions]
TT2:489 [binder, in GMu.Definitions]
TT2:55 [binder, in GMu.Preservation]
TT:103 [binder, in GMu.InfrastructureFV]
TT:122 [binder, in GMu.Regularity]
TT:127 [binder, in GMu.Preservation]
TT:132 [binder, in GMu.Regularity]
TT:136 [binder, in GMu.Regularity]
TT:137 [binder, in GMu.Preservation]
TT:147 [binder, in GMu.Preservation]
TT:16 [binder, in GMu.Preservation]
TT:163 [binder, in GMu.Preservation]
TT:173 [binder, in GMu.Preservation]
TT:182 [binder, in GMu.Preservation]
TT:190 [binder, in GMu.Preservation]
TT:23 [binder, in GMu.Preservation]
TT:32 [binder, in GMu.Preservation]
TT:4 [binder, in GMu.Tests]
TT:42 [binder, in GMu.Preservation]
TT:420 [binder, in GMu.Definitions]
TT:437 [binder, in GMu.Definitions]
TT:447 [binder, in GMu.Definitions]
TT:463 [binder, in GMu.Definitions]
TT:470 [binder, in GMu.Definitions]
TT:477 [binder, in GMu.Definitions]
TT:517 [binder, in GMu.Definitions]
TT:57 [binder, in GMu.Equations]
TT:583 [binder, in GMu.Definitions]
TT:588 [binder, in GMu.Definitions]
TT:63 [binder, in GMu.Equations]
TT:8 [binder, in GMu.Preservation]
TV:102 [binder, in GMu.InfrastructureFV]
two [definition, in GMu.TestVector]
two [definition, in GMu.Tests2]
typ [inductive, in GMu.Definitions]
typctx [definition, in GMu.Definitions]
typctx_elem [inductive, in GMu.Definitions]
type [inductive, in GMu.Definitions]
type_from_wft [lemma, in GMu.Regularity]
type_equation [inductive, in GMu.Definitions]
type_gadt [constructor, in GMu.Definitions]
type_all [constructor, in GMu.Definitions]
type_arrow [constructor, in GMu.Definitions]
type_tuple [constructor, in GMu.Definitions]
type_unit [constructor, in GMu.Definitions]
type_var [constructor, in GMu.Definitions]
type_closed [lemma, in GMu.InfrastructureOpen]
typing [inductive, in GMu.Definitions]
typing_implies_term [lemma, in GMu.Regularity]
typing_regular [lemma, in GMu.Regularity]
typing_exfalso [lemma, in GMu.Equations]
typing_eq [constructor, in GMu.Definitions]
typing_case [constructor, in GMu.Definitions]
typing_let [constructor, in GMu.Definitions]
typing_fix [constructor, in GMu.Definitions]
typing_snd [constructor, in GMu.Definitions]
typing_fst [constructor, in GMu.Definitions]
typing_tuple [constructor, in GMu.Definitions]
typing_tapp [constructor, in GMu.Definitions]
typing_tabs [constructor, in GMu.Definitions]
typing_app [constructor, in GMu.Definitions]
typing_abs [constructor, in GMu.Definitions]
typing_cons [constructor, in GMu.Definitions]
typing_var [constructor, in GMu.Definitions]
typing_unit [constructor, in GMu.Definitions]
typing_taint [inductive, in GMu.Definitions]
typing_replace_typ [lemma, in GMu.Preservation]
typing_replace_typ_gen [lemma, in GMu.Preservation]
typing_through_subst_te_many [lemma, in GMu.Preservation]
typing_through_subst_te_3 [lemma, in GMu.Preservation]
typing_through_subst_te_gen [lemma, in GMu.Preservation]
typing_through_subst_ee_fix [lemma, in GMu.Preservation]
typing_through_subst_ee_lam [lemma, in GMu.Preservation]
typing_weakening [lemma, in GMu.Preservation]
typing_weakening_delta_many [lemma, in GMu.Preservation]
typing_weakening_delta_many_eq [lemma, in GMu.Preservation]
typing_weakening_delta [lemma, in GMu.Preservation]
typing_weakening_delta_eq [lemma, in GMu.Preservation]
Typs:17 [binder, in GMu.CanonicalForms]
Typs:9 [binder, in GMu.CanonicalForms]
typ_size [definition, in GMu.Definitions]
typ_ind' [definition, in GMu.Definitions]
typ_ind'.typ_gadt_case [variable, in GMu.Definitions]
typ_ind'.typ_all_case [variable, in GMu.Definitions]
typ_ind'.typ_arrow_case [variable, in GMu.Definitions]
typ_ind'.typ_tuple_case [variable, in GMu.Definitions]
typ_ind'.typ_unit_case [variable, in GMu.Definitions]
typ_ind'.typ_fvar_case [variable, in GMu.Definitions]
typ_ind'.typ_bvar_case [variable, in GMu.Definitions]
typ_ind'.P [variable, in GMu.Definitions]
typ_ind' [section, in GMu.Definitions]
typ_gadt [constructor, in GMu.Definitions]
typ_all [constructor, in GMu.Definitions]
typ_arrow [constructor, in GMu.Definitions]
typ_tuple [constructor, in GMu.Definitions]
typ_unit [constructor, in GMu.Definitions]
typ_fvar [constructor, in GMu.Definitions]
typ_bvar [constructor, in GMu.Definitions]
typ_closed_in_surroundings [inductive, in GMu.InfrastructureOpen]
T':446 [binder, in GMu.Definitions]
T':64 [binder, in GMu.Equations]
T1:102 [binder, in GMu.Equations]
T1:12 [binder, in GMu.InfrastructureSubstPrim]
t1:13 [binder, in GMu.Definitions]
T1:15 [binder, in GMu.InfrastructureSubstPrim]
t1:16 [binder, in GMu.Definitions]
T1:162 [binder, in GMu.Preservation]
T1:172 [binder, in GMu.Preservation]
T1:177 [binder, in GMu.Definitions]
T1:179 [binder, in GMu.Definitions]
t1:19 [binder, in GMu.Definitions]
T1:20 [binder, in GMu.InfrastructureOpen]
T1:201 [binder, in GMu.SubstMatch]
T1:212 [binder, in GMu.SubstMatch]
T1:216 [binder, in GMu.SubstMatch]
T1:22 [binder, in GMu.CanonicalForms]
T1:221 [binder, in GMu.SubstMatch]
T1:23 [binder, in GMu.InfrastructureOpen]
T1:247 [binder, in GMu.SubstMatch]
T1:29 [binder, in GMu.CanonicalForms]
T1:305 [binder, in GMu.Definitions]
T1:309 [binder, in GMu.Definitions]
T1:31 [binder, in GMu.Zip]
T1:336 [binder, in GMu.Definitions]
T1:346 [binder, in GMu.Definitions]
T1:38 [binder, in GMu.Zip]
T1:4 [binder, in GMu.InfrastructureSubst]
T1:419 [binder, in GMu.Definitions]
T1:425 [binder, in GMu.Definitions]
T1:43 [binder, in GMu.SubstMatch]
T1:436 [binder, in GMu.Definitions]
T1:444 [binder, in GMu.Definitions]
T1:451 [binder, in GMu.Definitions]
T1:460 [binder, in GMu.Definitions]
T1:467 [binder, in GMu.Definitions]
T1:48 [binder, in GMu.SubstMatch]
T1:514 [binder, in GMu.Definitions]
T1:55 [binder, in GMu.Equations]
t1:56 [binder, in GMu.Definitions]
T1:61 [binder, in GMu.SubstMatch]
T1:65 [binder, in GMu.SubstMatch]
t1:66 [binder, in GMu.Definitions]
t1:66 [binder, in GMu.InfrastructureSubst]
T1:72 [binder, in GMu.InfrastructureFV]
T1:76 [binder, in GMu.Regularity2]
T1:8 [binder, in GMu.SubstMatch]
T1:82 [binder, in GMu.SubstMatch]
t1:82 [binder, in GMu.Definitions]
T1:89 [binder, in GMu.Regularity]
T1:9 [binder, in GMu.InfrastructureSubst]
T2:10 [binder, in GMu.InfrastructureSubst]
T2:103 [binder, in GMu.Equations]
T2:13 [binder, in GMu.InfrastructureSubstPrim]
t2:14 [binder, in GMu.Definitions]
T2:16 [binder, in GMu.InfrastructureSubstPrim]
T2:166 [binder, in GMu.Preservation]
t2:17 [binder, in GMu.Definitions]
T2:176 [binder, in GMu.Preservation]
T2:178 [binder, in GMu.Definitions]
T2:18 [binder, in GMu.InfrastructureSubst]
T2:180 [binder, in GMu.Definitions]
T2:182 [binder, in GMu.Definitions]
T2:202 [binder, in GMu.SubstMatch]
T2:21 [binder, in GMu.InfrastructureOpen]
T2:213 [binder, in GMu.SubstMatch]
T2:217 [binder, in GMu.SubstMatch]
T2:222 [binder, in GMu.SubstMatch]
T2:23 [binder, in GMu.CanonicalForms]
T2:24 [binder, in GMu.InfrastructureOpen]
T2:248 [binder, in GMu.SubstMatch]
T2:30 [binder, in GMu.CanonicalForms]
T2:306 [binder, in GMu.Definitions]
T2:310 [binder, in GMu.Definitions]
T2:314 [binder, in GMu.Definitions]
T2:32 [binder, in GMu.Zip]
T2:337 [binder, in GMu.Definitions]
T2:347 [binder, in GMu.Definitions]
T2:39 [binder, in GMu.Zip]
T2:426 [binder, in GMu.Definitions]
T2:44 [binder, in GMu.SubstMatch]
T2:452 [binder, in GMu.Definitions]
T2:461 [binder, in GMu.Definitions]
T2:468 [binder, in GMu.Definitions]
T2:485 [binder, in GMu.Definitions]
T2:49 [binder, in GMu.SubstMatch]
T2:5 [binder, in GMu.InfrastructureSubst]
T2:515 [binder, in GMu.Definitions]
T2:56 [binder, in GMu.Equations]
t2:57 [binder, in GMu.Definitions]
T2:62 [binder, in GMu.SubstMatch]
T2:66 [binder, in GMu.SubstMatch]
t2:67 [binder, in GMu.Definitions]
t2:67 [binder, in GMu.InfrastructureSubst]
T2:73 [binder, in GMu.InfrastructureFV]
T2:77 [binder, in GMu.Regularity2]
T2:83 [binder, in GMu.SubstMatch]
t2:83 [binder, in GMu.Definitions]
T2:9 [binder, in GMu.SubstMatch]
T:1 [binder, in GMu.Progress]
T:10 [binder, in GMu.InfrastructureSubstPrim]
t:101 [binder, in GMu.Definitions]
T:101 [binder, in GMu.InfrastructureFV]
T:102 [binder, in GMu.Regularity]
T:102 [binder, in GMu.Preservation]
T:103 [binder, in GMu.InfrastructureOpen]
T:106 [binder, in GMu.InfrastructureOpen]
T:109 [binder, in GMu.InfrastructureOpen]
T:109 [binder, in GMu.InfrastructureFV]
T:110 [binder, in GMu.InfrastructureFV]
T:111 [binder, in GMu.Regularity]
T:112 [binder, in GMu.Regularity]
T:113 [binder, in GMu.SubstMatch]
T:114 [binder, in GMu.InfrastructureFV]
T:116 [binder, in GMu.Regularity]
t:117 [binder, in GMu.Definitions]
T:118 [binder, in GMu.SubstMatch]
T:12 [binder, in GMu.InfrastructureFV]
T:121 [binder, in GMu.Regularity]
T:124 [binder, in GMu.SubstMatch]
T:125 [binder, in GMu.Prelude]
t:125 [binder, in GMu.Definitions]
T:125 [binder, in GMu.InfrastructureFV]
T:126 [binder, in GMu.Preservation]
T:128 [binder, in GMu.InfrastructureFV]
T:13 [binder, in GMu.TestVector]
T:130 [binder, in GMu.InfrastructureSubst]
T:131 [binder, in GMu.Regularity]
T:135 [binder, in GMu.InfrastructureOpen]
T:136 [binder, in GMu.Preservation]
T:136 [binder, in GMu.InfrastructureOpen]
T:137 [binder, in GMu.Prelude]
T:137 [binder, in GMu.Definitions]
T:138 [binder, in GMu.Regularity]
T:138 [binder, in GMu.InfrastructureOpen]
t:139 [binder, in GMu.Definitions]
T:139 [binder, in GMu.InfrastructureFV]
T:141 [binder, in GMu.Prelude]
t:141 [binder, in GMu.Definitions]
T:142 [binder, in GMu.SubstMatch]
T:144 [binder, in GMu.Prelude]
T:144 [binder, in GMu.Definitions]
T:145 [binder, in GMu.Preservation]
T:150 [binder, in GMu.InfrastructureFV]
T:152 [binder, in GMu.Definitions]
T:155 [binder, in GMu.Definitions]
T:156 [binder, in GMu.Prelude]
T:157 [binder, in GMu.InfrastructureFV]
T:159 [binder, in GMu.Definitions]
T:159 [binder, in GMu.InfrastructureFV]
T:16 [binder, in GMu.InfrastructureSubst]
T:16 [binder, in GMu.CanonicalForms]
T:160 [binder, in GMu.InfrastructureSubst]
T:166 [binder, in GMu.Definitions]
T:166 [binder, in GMu.InfrastructureFV]
T:17 [binder, in GMu.Regularity]
T:17 [binder, in GMu.Equations]
T:171 [binder, in GMu.InfrastructureSubst]
T:173 [binder, in GMu.Definitions]
T:183 [binder, in GMu.InfrastructureSubst]
T:183 [binder, in GMu.Preservation]
t:191 [binder, in GMu.Prelude]
T:194 [binder, in GMu.Preservation]
T:2 [binder, in GMu.Progress]
T:2 [binder, in GMu.InfrastructureSubstPrim]
T:20 [binder, in GMu.InfrastructureSubstPrim]
T:201 [binder, in GMu.Preservation]
T:21 [binder, in GMu.InfrastructureSubst]
T:210 [binder, in GMu.Preservation]
T:211 [binder, in GMu.Preservation]
T:212 [binder, in GMu.Preservation]
T:213 [binder, in GMu.Preservation]
T:214 [binder, in GMu.Definitions]
T:214 [binder, in GMu.Preservation]
T:215 [binder, in GMu.Preservation]
T:216 [binder, in GMu.Preservation]
T:217 [binder, in GMu.Preservation]
T:218 [binder, in GMu.SubstMatch]
T:218 [binder, in GMu.Preservation]
T:219 [binder, in GMu.Preservation]
T:23 [binder, in GMu.InfrastructureSubstPrim]
T:234 [binder, in GMu.SubstMatch]
t:24 [binder, in GMu.Definitions]
T:24 [binder, in GMu.TestCommon]
T:250 [binder, in GMu.Definitions]
T:26 [binder, in GMu.Regularity]
T:26 [binder, in GMu.InfrastructureSubst]
T:26 [binder, in GMu.InfrastructureOpen]
T:270 [binder, in GMu.Definitions]
T:279 [binder, in GMu.Definitions]
T:3 [binder, in GMu.Regularity]
T:3 [binder, in GMu.Equations]
T:3 [binder, in GMu.InfrastructureSubst]
T:3 [binder, in GMu.Tests]
T:31 [binder, in GMu.Regularity]
T:31 [binder, in GMu.InfrastructureOpen]
T:31 [binder, in GMu.TestCommon]
T:322 [binder, in GMu.Definitions]
T:323 [binder, in GMu.Definitions]
T:333 [binder, in GMu.Definitions]
T:35 [binder, in GMu.CanonicalForms]
T:35 [binder, in GMu.InfrastructureOpen]
T:36 [binder, in GMu.InfrastructureOpen]
T:37 [binder, in GMu.Regularity]
T:379 [binder, in GMu.Definitions]
T:39 [binder, in GMu.Regularity2]
T:396 [binder, in GMu.Definitions]
t:4 [binder, in GMu.Definitions]
T:40 [binder, in GMu.InfrastructureOpen]
T:41 [binder, in GMu.Prelude]
T:41 [binder, in GMu.Preservation]
T:41 [binder, in GMu.InfrastructureFV]
T:412 [binder, in GMu.Definitions]
T:42 [binder, in GMu.Prelude]
T:42 [binder, in GMu.InfrastructureSubst]
T:43 [binder, in GMu.Prelude]
T:445 [binder, in GMu.Definitions]
T:45 [binder, in GMu.Regularity2]
T:47 [binder, in GMu.Regularity]
T:475 [binder, in GMu.Definitions]
T:498 [binder, in GMu.Definitions]
T:5 [binder, in GMu.Equations]
T:51 [binder, in GMu.Regularity2]
T:51 [binder, in GMu.SubstMatch]
T:51 [binder, in GMu.InfrastructureFV]
T:52 [binder, in GMu.InfrastructureSubst]
T:520 [binder, in GMu.Definitions]
T:525 [binder, in GMu.Definitions]
T:53 [binder, in GMu.Regularity]
T:53 [binder, in GMu.Preservation]
T:534 [binder, in GMu.Definitions]
T:54 [binder, in GMu.Prelude]
T:54 [binder, in GMu.InfrastructureFV]
T:557 [binder, in GMu.Definitions]
T:57 [binder, in GMu.InfrastructureFV]
T:58 [binder, in GMu.Regularity2]
T:586 [binder, in GMu.Definitions]
T:59 [binder, in GMu.InfrastructureOpen]
T:591 [binder, in GMu.Definitions]
T:6 [binder, in GMu.InfrastructureSubstPrim]
T:60 [binder, in GMu.InfrastructureFV]
T:62 [binder, in GMu.Equations]
T:63 [binder, in GMu.Definitions]
T:64 [binder, in GMu.InfrastructureFV]
T:67 [binder, in GMu.InfrastructureOpen]
T:68 [binder, in GMu.InfrastructureFV]
T:70 [binder, in GMu.InfrastructureOpen]
T:70 [binder, in GMu.InfrastructureFV]
T:71 [binder, in GMu.Regularity]
T:72 [binder, in GMu.Definitions]
T:74 [binder, in GMu.Regularity]
T:75 [binder, in GMu.Definitions]
T:77 [binder, in GMu.SubstMatch]
T:78 [binder, in GMu.InfrastructureFV]
T:79 [binder, in GMu.Regularity]
T:8 [binder, in GMu.Equations]
T:8 [binder, in GMu.CanonicalForms]
T:8 [binder, in GMu.InfrastructureOpen]
T:82 [binder, in GMu.InfrastructureFV]
T:85 [binder, in GMu.Regularity]
T:85 [binder, in GMu.Equations]
t:85 [binder, in GMu.Definitions]
T:86 [binder, in GMu.InfrastructureFV]
T:88 [binder, in GMu.Prelude]
t:9 [binder, in GMu.TestVector]
T:91 [binder, in GMu.Prelude]
T:91 [binder, in GMu.InfrastructureFV]
T:92 [binder, in GMu.Equations]
T:96 [binder, in GMu.SubstMatch]
T:96 [binder, in GMu.InfrastructureSubst]
T:99 [binder, in GMu.Equations]
T:99 [binder, in GMu.InfrastructureFV]

U

Uh:31 [binder, in GMu.InfrastructureSubst]
Uh:37 [binder, in GMu.InfrastructureSubst]
union_empty [lemma, in GMu.Prelude]
union_distributes [lemma, in GMu.Prelude]
union_fold_detach [lemma, in GMu.Prelude]
union_distribute [lemma, in GMu.Prelude]
Us:100 [binder, in GMu.Regularity]
Us:138 [binder, in GMu.InfrastructureSubst]
Us:153 [binder, in GMu.InfrastructureSubst]
Us:156 [binder, in GMu.InfrastructureFV]
Us:169 [binder, in GMu.Prelude]
Us:193 [binder, in GMu.Preservation]
Us:198 [binder, in GMu.Preservation]
Us:211 [binder, in GMu.SubstMatch]
Us:23 [binder, in GMu.TestCommon]
Us:269 [binder, in GMu.Definitions]
Us:29 [binder, in GMu.TestCommon]
Us:381 [binder, in GMu.Definitions]
Us:43 [binder, in GMu.InfrastructureSubst]
Us:580 [binder, in GMu.Definitions]
Us:62 [binder, in GMu.Regularity2]
Us:90 [binder, in GMu.Equations]
Us:98 [binder, in GMu.Equations]
Ut:32 [binder, in GMu.InfrastructureSubst]
Ut:38 [binder, in GMu.InfrastructureSubst]
uvec2 [definition, in GMu.TestVector]
uvec2_type [lemma, in GMu.TestVector]
U0:110 [binder, in GMu.Preservation]
U0:116 [binder, in GMu.Preservation]
U0:137 [binder, in GMu.SubstMatch]
U0:139 [binder, in GMu.SubstMatch]
U0:154 [binder, in GMu.SubstMatch]
U0:156 [binder, in GMu.SubstMatch]
U0:167 [binder, in GMu.SubstMatch]
U0:169 [binder, in GMu.SubstMatch]
U0:226 [binder, in GMu.SubstMatch]
U0:228 [binder, in GMu.SubstMatch]
U0:61 [binder, in GMu.Preservation]
U0:67 [binder, in GMu.Preservation]
U0:73 [binder, in GMu.Preservation]
U0:79 [binder, in GMu.Preservation]
U0:87 [binder, in GMu.Preservation]
U0:93 [binder, in GMu.Preservation]
U1:184 [binder, in GMu.Preservation]
U1:240 [binder, in GMu.SubstMatch]
U1:245 [binder, in GMu.SubstMatch]
U1:45 [binder, in GMu.SubstMatch]
U2:185 [binder, in GMu.Preservation]
U2:241 [binder, in GMu.SubstMatch]
U2:246 [binder, in GMu.SubstMatch]
U2:46 [binder, in GMu.SubstMatch]
u:1 [binder, in GMu.Preservation]
U:100 [binder, in GMu.Equations]
U:100 [binder, in GMu.Preservation]
U:103 [binder, in GMu.Regularity]
U:108 [binder, in GMu.Regularity]
U:11 [binder, in GMu.Regularity]
U:113 [binder, in GMu.InfrastructureOpen]
u:116 [binder, in GMu.Definitions]
u:118 [binder, in GMu.InfrastructureOpen]
u:121 [binder, in GMu.Definitions]
U:123 [binder, in GMu.InfrastructureSubst]
u:123 [binder, in GMu.InfrastructureOpen]
u:124 [binder, in GMu.Definitions]
U:126 [binder, in GMu.SubstMatch]
U:126 [binder, in GMu.Prelude]
u:127 [binder, in GMu.InfrastructureOpen]
U:128 [binder, in GMu.InfrastructureSubst]
U:129 [binder, in GMu.SubstMatch]
u:129 [binder, in GMu.InfrastructureOpen]
U:129 [binder, in GMu.InfrastructureFV]
u:131 [binder, in GMu.Definitions]
U:131 [binder, in GMu.InfrastructureSubst]
U:135 [binder, in GMu.SubstMatch]
U:136 [binder, in GMu.InfrastructureSubst]
U:138 [binder, in GMu.Definitions]
U:14 [binder, in GMu.Preservation]
U:140 [binder, in GMu.Definitions]
u:142 [binder, in GMu.Definitions]
U:145 [binder, in GMu.SubstMatch]
U:145 [binder, in GMu.InfrastructureFV]
U:15 [binder, in GMu.Equations]
U:15 [binder, in GMu.InfrastructureSubst]
U:152 [binder, in GMu.SubstMatch]
U:156 [binder, in GMu.InfrastructureSubst]
U:157 [binder, in GMu.InfrastructureSubst]
U:158 [binder, in GMu.InfrastructureFV]
U:159 [binder, in GMu.SubstMatch]
U:16 [binder, in GMu.Regularity]
U:160 [binder, in GMu.InfrastructureFV]
U:165 [binder, in GMu.SubstMatch]
U:165 [binder, in GMu.Preservation]
U:17 [binder, in GMu.SubstMatch]
U:172 [binder, in GMu.SubstMatch]
U:175 [binder, in GMu.Preservation]
U:179 [binder, in GMu.SubstMatch]
U:18 [binder, in GMu.Equations]
U:180 [binder, in GMu.InfrastructureSubst]
U:189 [binder, in GMu.SubstMatch]
U:19 [binder, in GMu.InfrastructureSubst]
U:195 [binder, in GMu.Preservation]
U:2 [binder, in GMu.InfrastructureSubst]
U:204 [binder, in GMu.SubstMatch]
U:206 [binder, in GMu.SubstMatch]
u:21 [binder, in GMu.Preservation]
U:22 [binder, in GMu.SubstMatch]
U:22 [binder, in GMu.Preservation]
U:24 [binder, in GMu.InfrastructureSubstPrim]
U:249 [binder, in GMu.Definitions]
U:25 [binder, in GMu.TestCommon]
U:254 [binder, in GMu.Definitions]
u:260 [binder, in GMu.Definitions]
U:28 [binder, in GMu.SubstMatch]
U:280 [binder, in GMu.Definitions]
u:30 [binder, in GMu.Preservation]
U:31 [binder, in GMu.Preservation]
U:32 [binder, in GMu.TestCommon]
U:34 [binder, in GMu.InfrastructureSubst]
U:35 [binder, in GMu.InfrastructureSubst]
U:37 [binder, in GMu.InfrastructureOpen]
U:382 [binder, in GMu.Definitions]
U:39 [binder, in GMu.SubstMatch]
U:40 [binder, in GMu.InfrastructureSubst]
U:41 [binder, in GMu.InfrastructureOpen]
U:46 [binder, in GMu.InfrastructureSubst]
U:47 [binder, in GMu.InfrastructureSubst]
U:49 [binder, in GMu.InfrastructureSubst]
u:50 [binder, in GMu.Preservation]
U:51 [binder, in GMu.Preservation]
U:52 [binder, in GMu.InfrastructureFV]
U:53 [binder, in GMu.SubstMatch]
U:54 [binder, in GMu.InfrastructureSubst]
U:55 [binder, in GMu.InfrastructureFV]
U:57 [binder, in GMu.SubstMatch]
U:57 [binder, in GMu.InfrastructureSubst]
U:576 [binder, in GMu.Definitions]
U:58 [binder, in GMu.InfrastructureFV]
U:59 [binder, in GMu.Regularity]
U:6 [binder, in GMu.Equations]
U:6 [binder, in GMu.Preservation]
U:60 [binder, in GMu.InfrastructureSubst]
U:61 [binder, in GMu.InfrastructureFV]
U:63 [binder, in GMu.Regularity2]
u:64 [binder, in GMu.InfrastructureSubst]
U:68 [binder, in GMu.SubstMatch]
u:68 [binder, in GMu.InfrastructureSubst]
U:70 [binder, in GMu.SubstMatch]
U:70 [binder, in GMu.Equations]
u:75 [binder, in GMu.InfrastructureSubst]
u:79 [binder, in GMu.InfrastructureSubst]
U:8 [binder, in GMu.InfrastructureSubstPrim]
U:86 [binder, in GMu.Equations]
U:88 [binder, in GMu.SubstMatch]
U:88 [binder, in GMu.Regularity]
u:88 [binder, in GMu.InfrastructureSubst]
U:9 [binder, in GMu.Equations]
u:9 [binder, in GMu.Preservation]
U:93 [binder, in GMu.Equations]
u:99 [binder, in GMu.Preservation]

V

value [inductive, in GMu.Definitions]
value_regular [lemma, in GMu.Prelude]
value_is_term [lemma, in GMu.Prelude]
value_gadt [constructor, in GMu.Definitions]
value_tuple [constructor, in GMu.Definitions]
value_lamvar [constructor, in GMu.Definitions]
value_unit [constructor, in GMu.Definitions]
value_tabs [constructor, in GMu.Definitions]
value_abs [constructor, in GMu.Definitions]
var_kind [inductive, in GMu.Definitions]
Vector [axiom, in GMu.TestVector]
VectorDef [definition, in GMu.TestVector]
vk0:109 [binder, in GMu.Preservation]
vk0:115 [binder, in GMu.Preservation]
vk0:60 [binder, in GMu.Preservation]
vk0:66 [binder, in GMu.Preservation]
vk0:72 [binder, in GMu.Preservation]
vk0:78 [binder, in GMu.Preservation]
vk0:86 [binder, in GMu.Preservation]
vk0:92 [binder, in GMu.Preservation]
vk:10 [binder, in GMu.Regularity]
vk:124 [binder, in GMu.InfrastructureFV]
vk:161 [binder, in GMu.Preservation]
vk:166 [binder, in GMu.InfrastructureSubst]
vk:171 [binder, in GMu.Preservation]
vk:191 [binder, in GMu.Definitions]
vk:378 [binder, in GMu.Definitions]
vk:395 [binder, in GMu.Definitions]
vk:4 [binder, in GMu.InfrastructureOpen]
vk:46 [binder, in GMu.Regularity]
vk:48 [binder, in GMu.InfrastructureOpen]
vk:50 [binder, in GMu.Regularity2]
vk:52 [binder, in GMu.Regularity]
vk:57 [binder, in GMu.Regularity2]
vk:58 [binder, in GMu.Regularity]
vk:70 [binder, in GMu.Regularity]
vk:71 [binder, in GMu.InfrastructureSubst]
vk:75 [binder, in GMu.Regularity2]
vk:77 [binder, in GMu.InfrastructureSubst]
vk:83 [binder, in GMu.InfrastructureSubst]
vk:85 [binder, in GMu.InfrastructureFV]
vk:90 [binder, in GMu.InfrastructureOpen]
vk:90 [binder, in GMu.InfrastructureFV]
Vs:199 [binder, in GMu.Preservation]
v1:109 [binder, in GMu.Prelude]
V1:132 [binder, in GMu.SubstMatch]
V1:149 [binder, in GMu.SubstMatch]
V1:162 [binder, in GMu.SubstMatch]
V1:176 [binder, in GMu.SubstMatch]
v1:211 [binder, in GMu.Definitions]
v1:215 [binder, in GMu.Definitions]
v1:24 [binder, in GMu.CanonicalForms]
v1:31 [binder, in GMu.CanonicalForms]
v1:36 [binder, in GMu.CanonicalForms]
v1:527 [binder, in GMu.Definitions]
v1:530 [binder, in GMu.Definitions]
v1:532 [binder, in GMu.Definitions]
v1:552 [binder, in GMu.Definitions]
v1:565 [binder, in GMu.Definitions]
v2:110 [binder, in GMu.Prelude]
V2:133 [binder, in GMu.SubstMatch]
V2:150 [binder, in GMu.SubstMatch]
V2:163 [binder, in GMu.SubstMatch]
V2:177 [binder, in GMu.SubstMatch]
v2:25 [binder, in GMu.CanonicalForms]
v2:522 [binder, in GMu.Definitions]
v2:531 [binder, in GMu.Definitions]
v2:533 [binder, in GMu.Definitions]
V:10 [binder, in GMu.Equations]
V:101 [binder, in GMu.InfrastructureSubst]
v:106 [binder, in GMu.InfrastructureSubst]
v:117 [binder, in GMu.InfrastructureOpen]
V:122 [binder, in GMu.InfrastructureOpen]
V:143 [binder, in GMu.InfrastructureSubst]
V:149 [binder, in GMu.InfrastructureSubst]
V:191 [binder, in GMu.Preservation]
V:202 [binder, in GMu.Definitions]
V:212 [binder, in GMu.Definitions]
V:22 [binder, in GMu.InfrastructureSubst]
V:230 [binder, in GMu.Definitions]
V:28 [binder, in GMu.InfrastructureSubst]
V:31 [binder, in GMu.SubstMatch]
V:383 [binder, in GMu.Definitions]
V:417 [binder, in GMu.Definitions]
v:47 [binder, in GMu.CanonicalForms]
v:476 [binder, in GMu.Definitions]
V:484 [binder, in GMu.Definitions]
v:535 [binder, in GMu.Definitions]

W

well_formed_id [lemma, in GMu.Tests]
well_typed_id [lemma, in GMu.Tests]
wft [inductive, in GMu.Definitions]
wft_subst_tb_3 [lemma, in GMu.Regularity2]
wft_subst_tb_2 [lemma, in GMu.Regularity2]
wft_weaken_simple [lemma, in GMu.Regularity2]
wft_subst_matching [lemma, in GMu.SubstMatch]
wft_subst_matching_gen [lemma, in GMu.SubstMatch]
wft_open_many [lemma, in GMu.Regularity]
wft_subst_tb_many [lemma, in GMu.Regularity]
wft_open [lemma, in GMu.Regularity]
wft_subst_tb [lemma, in GMu.Regularity]
wft_weaken [lemma, in GMu.Regularity]
wft_type [lemma, in GMu.Regularity]
wft_strengthen_typ_many [lemma, in GMu.Regularity]
wft_strengthen_equations [lemma, in GMu.Regularity]
wft_strengthen_equation [lemma, in GMu.Regularity]
wft_strengthen_typ [lemma, in GMu.Regularity]
wft_from_env_has_typ [lemma, in GMu.Regularity]
wft_gadt [constructor, in GMu.Definitions]
wft_all [constructor, in GMu.Definitions]
wft_tuple [constructor, in GMu.Definitions]
wft_arrow [constructor, in GMu.Definitions]
wft_var [constructor, in GMu.Definitions]
wft_unit [constructor, in GMu.Definitions]
wft_gives_fv [lemma, in GMu.InfrastructureFV]

X

Xs:104 [binder, in GMu.InfrastructureSubst]
Xs:131 [binder, in GMu.InfrastructureFV]
Xs:137 [binder, in GMu.InfrastructureSubst]
Xs:141 [binder, in GMu.InfrastructureSubst]
Xs:146 [binder, in GMu.InfrastructureSubst]
Xs:151 [binder, in GMu.InfrastructureSubst]
Xs:20 [binder, in GMu.InfrastructureSubst]
Xs:25 [binder, in GMu.InfrastructureSubst]
Xs:268 [binder, in GMu.Definitions]
Xs:343 [binder, in GMu.Definitions]
Xs:41 [binder, in GMu.InfrastructureSubst]
Xs:579 [binder, in GMu.Definitions]
Xs:99 [binder, in GMu.InfrastructureSubst]
x0:108 [binder, in GMu.Preservation]
x0:114 [binder, in GMu.Preservation]
X0:136 [binder, in GMu.SubstMatch]
X0:138 [binder, in GMu.SubstMatch]
X0:153 [binder, in GMu.SubstMatch]
X0:155 [binder, in GMu.SubstMatch]
X0:166 [binder, in GMu.SubstMatch]
X0:168 [binder, in GMu.SubstMatch]
x0:59 [binder, in GMu.Preservation]
x0:65 [binder, in GMu.Preservation]
x0:71 [binder, in GMu.Preservation]
x0:77 [binder, in GMu.Preservation]
x0:85 [binder, in GMu.Preservation]
x0:91 [binder, in GMu.Preservation]
x:10 [binder, in GMu.Definitions]
x:10 [binder, in GMu.TestCommon]
X:103 [binder, in GMu.InfrastructureSubst]
X:105 [binder, in GMu.Preservation]
x:106 [binder, in GMu.Prelude]
X:107 [binder, in GMu.InfrastructureFV]
x:108 [binder, in GMu.Prelude]
x:11 [binder, in GMu.TestVector]
X:11 [binder, in GMu.InfrastructureSubst]
x:11 [binder, in GMu.InfrastructureOpen]
x:11 [binder, in GMu.TestCommon]
X:111 [binder, in GMu.Preservation]
X:111 [binder, in GMu.InfrastructureFV]
X:115 [binder, in GMu.Regularity]
X:115 [binder, in GMu.InfrastructureFV]
x:12 [binder, in GMu.InfrastructureOpen]
x:12 [binder, in GMu.TestCommon]
x:120 [binder, in GMu.InfrastructureFV]
X:123 [binder, in GMu.Regularity]
x:123 [binder, in GMu.Prelude]
x:123 [binder, in GMu.InfrastructureFV]
X:124 [binder, in GMu.Regularity]
X:125 [binder, in GMu.SubstMatch]
X:127 [binder, in GMu.InfrastructureFV]
X:128 [binder, in GMu.Preservation]
X:129 [binder, in GMu.Preservation]
X:13 [binder, in GMu.Regularity2]
X:13 [binder, in GMu.InfrastructureSubst]
x:13 [binder, in GMu.TestCommon]
x:130 [binder, in GMu.Prelude]
X:131 [binder, in GMu.SubstMatch]
X:134 [binder, in GMu.SubstMatch]
x:134 [binder, in GMu.InfrastructureFV]
x:136 [binder, in GMu.InfrastructureFV]
X:14 [binder, in GMu.Equations]
X:144 [binder, in GMu.InfrastructureFV]
x:145 [binder, in GMu.Prelude]
X:145 [binder, in GMu.InfrastructureSubst]
X:148 [binder, in GMu.SubstMatch]
x:148 [binder, in GMu.Prelude]
x:15 [binder, in GMu.TestCommon]
x:150 [binder, in GMu.Prelude]
X:150 [binder, in GMu.InfrastructureSubst]
X:151 [binder, in GMu.SubstMatch]
x:152 [binder, in GMu.Prelude]
x:154 [binder, in GMu.Prelude]
X:154 [binder, in GMu.InfrastructureSubst]
X:155 [binder, in GMu.InfrastructureSubst]
x:160 [binder, in GMu.Preservation]
X:161 [binder, in GMu.SubstMatch]
X:164 [binder, in GMu.SubstMatch]
x:165 [binder, in GMu.InfrastructureSubst]
x:165 [binder, in GMu.InfrastructureFV]
X:17 [binder, in GMu.InfrastructureSubst]
X:17 [binder, in GMu.InfrastructureOpen]
x:17 [binder, in GMu.TestCommon]
x:170 [binder, in GMu.Preservation]
x:172 [binder, in GMu.InfrastructureFV]
X:175 [binder, in GMu.SubstMatch]
X:176 [binder, in GMu.Definitions]
X:178 [binder, in GMu.SubstMatch]
X:179 [binder, in GMu.InfrastructureSubst]
X:18 [binder, in GMu.Regularity]
x:18 [binder, in GMu.TestCommon]
X:183 [binder, in GMu.Definitions]
x:185 [binder, in GMu.InfrastructureFV]
X:188 [binder, in GMu.SubstMatch]
x:19 [binder, in GMu.Equations]
x:192 [binder, in GMu.Definitions]
x:2 [binder, in GMu.Prelude]
x:2 [binder, in GMu.InfrastructureOpen]
x:2 [binder, in GMu.InfrastructureFV]
X:20 [binder, in GMu.Regularity]
x:202 [binder, in GMu.Preservation]
X:203 [binder, in GMu.SubstMatch]
x:203 [binder, in GMu.Preservation]
x:204 [binder, in GMu.Definitions]
x:204 [binder, in GMu.Preservation]
X:205 [binder, in GMu.SubstMatch]
x:205 [binder, in GMu.Preservation]
x:206 [binder, in GMu.Preservation]
x:207 [binder, in GMu.Preservation]
X:209 [binder, in GMu.Definitions]
X:21 [binder, in GMu.SubstMatch]
x:21 [binder, in GMu.Equations]
X:210 [binder, in GMu.Definitions]
x:216 [binder, in GMu.Definitions]
x:217 [binder, in GMu.Definitions]
x:220 [binder, in GMu.Preservation]
x:221 [binder, in GMu.Definitions]
x:221 [binder, in GMu.Preservation]
X:225 [binder, in GMu.SubstMatch]
X:227 [binder, in GMu.SubstMatch]
x:228 [binder, in GMu.Definitions]
x:23 [binder, in GMu.Equations]
x:233 [binder, in GMu.Definitions]
X:24 [binder, in GMu.InfrastructureSubst]
X:25 [binder, in GMu.SubstMatch]
x:25 [binder, in GMu.Equations]
X:286 [binder, in GMu.Definitions]
X:29 [binder, in GMu.InfrastructureSubst]
x:3 [binder, in GMu.Prelude]
X:302 [binder, in GMu.Definitions]
X:315 [binder, in GMu.Definitions]
X:32 [binder, in GMu.InfrastructureOpen]
X:36 [binder, in GMu.SubstMatch]
x:37 [binder, in GMu.InfrastructureFV]
x:377 [binder, in GMu.Definitions]
x:394 [binder, in GMu.Definitions]
x:4 [binder, in GMu.Prelude]
x:421 [binder, in GMu.Definitions]
X:438 [binder, in GMu.Definitions]
X:439 [binder, in GMu.Definitions]
X:44 [binder, in GMu.InfrastructureSubst]
x:45 [binder, in GMu.Regularity]
X:45 [binder, in GMu.InfrastructureSubst]
x:46 [binder, in GMu.InfrastructureFV]
x:47 [binder, in GMu.Prelude]
x:47 [binder, in GMu.InfrastructureOpen]
x:478 [binder, in GMu.Definitions]
x:479 [binder, in GMu.Definitions]
X:48 [binder, in GMu.InfrastructureSubst]
x:49 [binder, in GMu.Regularity2]
x:49 [binder, in GMu.Definitions]
x:49 [binder, in GMu.Preservation]
x:490 [binder, in GMu.Definitions]
x:5 [binder, in GMu.Prelude]
x:509 [binder, in GMu.Definitions]
x:51 [binder, in GMu.Regularity]
X:53 [binder, in GMu.InfrastructureSubst]
X:55 [binder, in GMu.InfrastructureSubst]
x:56 [binder, in GMu.Regularity2]
X:56 [binder, in GMu.SubstMatch]
X:56 [binder, in GMu.Preservation]
x:57 [binder, in GMu.Regularity]
X:59 [binder, in GMu.InfrastructureSubst]
x:6 [binder, in GMu.Prelude]
X:6 [binder, in GMu.InfrastructureSubst]
x:6 [binder, in GMu.InfrastructureOpen]
x:62 [binder, in GMu.InfrastructureSubst]
X:62 [binder, in GMu.Preservation]
X:65 [binder, in GMu.Regularity]
X:65 [binder, in GMu.InfrastructureFV]
X:67 [binder, in GMu.SubstMatch]
X:67 [binder, in GMu.InfrastructureFV]
x:68 [binder, in GMu.Prelude]
X:68 [binder, in GMu.Preservation]
x:69 [binder, in GMu.Regularity]
x:7 [binder, in GMu.Prelude]
X:7 [binder, in GMu.InfrastructureSubstPrim]
x:70 [binder, in GMu.InfrastructureSubst]
x:71 [binder, in GMu.Prelude]
x:71 [binder, in GMu.InfrastructureFV]
x:72 [binder, in GMu.InfrastructureSubst]
x:74 [binder, in GMu.Regularity2]
X:74 [binder, in GMu.Preservation]
X:76 [binder, in GMu.SubstMatch]
x:77 [binder, in GMu.InfrastructureFV]
x:78 [binder, in GMu.InfrastructureSubst]
x:8 [binder, in GMu.Prelude]
x:8 [binder, in GMu.InfrastructureFV]
x:81 [binder, in GMu.InfrastructureFV]
X:82 [binder, in GMu.Preservation]
x:84 [binder, in GMu.InfrastructureSubst]
x:84 [binder, in GMu.InfrastructureFV]
x:85 [binder, in GMu.Prelude]
X:85 [binder, in GMu.InfrastructureOpen]
x:86 [binder, in GMu.Prelude]
X:87 [binder, in GMu.SubstMatch]
X:88 [binder, in GMu.Preservation]
X:88 [binder, in GMu.InfrastructureFV]
x:89 [binder, in GMu.Prelude]
x:89 [binder, in GMu.InfrastructureOpen]
x:89 [binder, in GMu.InfrastructureFV]
x:9 [binder, in GMu.Regularity]
x:9 [binder, in GMu.Prelude]
X:9 [binder, in GMu.InfrastructureOpen]
X:90 [binder, in GMu.InfrastructureSubst]
X:91 [binder, in GMu.SubstMatch]
x:92 [binder, in GMu.Prelude]
X:94 [binder, in GMu.InfrastructureFV]
X:95 [binder, in GMu.SubstMatch]
x:97 [binder, in GMu.Prelude]
X:97 [binder, in GMu.InfrastructureFV]
X:98 [binder, in GMu.SubstMatch]
x:98 [binder, in GMu.Preservation]
x:98 [binder, in GMu.InfrastructureOpen]
x:99 [binder, in GMu.InfrastructureOpen]

Y

Y:102 [binder, in GMu.InfrastructureSubst]
y:107 [binder, in GMu.InfrastructureSubst]
y:124 [binder, in GMu.Prelude]
Y:13 [binder, in GMu.SubstMatch]
Y:14 [binder, in GMu.InfrastructureSubst]
Y:144 [binder, in GMu.InfrastructureSubst]
Y:148 [binder, in GMu.InfrastructureSubst]
Y:15 [binder, in GMu.Preservation]
y:16 [binder, in GMu.TestCommon]
Y:23 [binder, in GMu.InfrastructureSubst]
Y:27 [binder, in GMu.InfrastructureSubst]
Y:30 [binder, in GMu.SubstMatch]
Y:50 [binder, in GMu.SubstMatch]
Y:56 [binder, in GMu.InfrastructureSubst]
Y:66 [binder, in GMu.InfrastructureFV]
Y:68 [binder, in GMu.Equations]
y:73 [binder, in GMu.InfrastructureSubst]
Y:81 [binder, in GMu.SubstMatch]
y:87 [binder, in GMu.Prelude]
y:90 [binder, in GMu.Prelude]

Z

Zero [axiom, in GMu.TestVector]
zero [definition, in GMu.Tests2]
zero_type [lemma, in GMu.Tests2]
zip [definition, in GMu.Zip]
Zip [section, in GMu.Zip]
Zip [library]
zipWith [definition, in GMu.Zip]
zipWithIsMappedZip [lemma, in GMu.Zip]
zip_types [lemma, in GMu.TestVector]
zip_typ [definition, in GMu.TestVector]
zip_trm [definition, in GMu.TestVector]
zip_swap [lemma, in GMu.Zip]
Zip.A [variable, in GMu.Zip]
Zip.B [variable, in GMu.Zip]
Zip.R [variable, in GMu.Zip]
z':62 [binder, in GMu.Prelude]
Z:1 [binder, in GMu.InfrastructureSubst]
Z:106 [binder, in GMu.InfrastructureFV]
Z:110 [binder, in GMu.InfrastructureSubst]
Z:112 [binder, in GMu.InfrastructureFV]
Z:113 [binder, in GMu.InfrastructureSubst]
Z:116 [binder, in GMu.InfrastructureSubst]
Z:116 [binder, in GMu.InfrastructureFV]
z:117 [binder, in GMu.Prelude]
Z:120 [binder, in GMu.InfrastructureSubst]
Z:121 [binder, in GMu.InfrastructureFV]
Z:123 [binder, in GMu.Preservation]
Z:124 [binder, in GMu.InfrastructureSubst]
Z:127 [binder, in GMu.InfrastructureSubst]
Z:13 [binder, in GMu.InfrastructureFV]
Z:132 [binder, in GMu.InfrastructureSubst]
Z:133 [binder, in GMu.Preservation]
Z:134 [binder, in GMu.InfrastructureSubst]
Z:164 [binder, in GMu.Definitions]
Z:169 [binder, in GMu.InfrastructureSubst]
Z:179 [binder, in GMu.InfrastructureFV]
Z:183 [binder, in GMu.InfrastructureFV]
Z:185 [binder, in GMu.InfrastructureSubst]
Z:187 [binder, in GMu.InfrastructureFV]
Z:188 [binder, in GMu.InfrastructureSubst]
Z:199 [binder, in GMu.SubstMatch]
Z:21 [binder, in GMu.InfrastructureFV]
Z:248 [binder, in GMu.Definitions]
Z:253 [binder, in GMu.Definitions]
z:258 [binder, in GMu.Definitions]
Z:264 [binder, in GMu.Definitions]
Z:28 [binder, in GMu.InfrastructureFV]
Z:36 [binder, in GMu.InfrastructureFV]
Z:37 [binder, in GMu.Regularity2]
Z:43 [binder, in GMu.Regularity2]
z:45 [binder, in GMu.InfrastructureFV]
Z:59 [binder, in GMu.Regularity2]
z:61 [binder, in GMu.Prelude]
Z:68 [binder, in GMu.Regularity2]
Z:81 [binder, in GMu.InfrastructureSubst]
Z:83 [binder, in GMu.Regularity]
z:86 [binder, in GMu.InfrastructureSubst]
Z:92 [binder, in GMu.InfrastructureSubst]
Z:97 [binder, in GMu.InfrastructureSubst]

other

case_pattern:_ => _ (L2GMu) [notation, in GMu.Notations]
[ _ ; _ ; .. ; _ ]* (list_scope) [notation, in GMu.Definitions]
[ _ ]* (list_scope) [notation, in GMu.Definitions]
[ ]* (list_scope) [notation, in GMu.Definitions]
_ <|| _ (L2GMu) [notation, in GMu.Notations]
_ <| _ (L2GMu) [notation, in GMu.Notations]
_ ==> _ (L2GMu) [notation, in GMu.Notations]
_ ** _ (L2GMu) [notation, in GMu.Notations]
case _ as _ of { _ | .. | _ } (L2GMu) [notation, in GMu.Notations]
enum _ {{ _ | .. | _ }} (L2GMu) [notation, in GMu.Notations]
fixs _ => _ (L2GMu) [notation, in GMu.Notations]
fst( _ ) (L2GMu) [notation, in GMu.Notations]
lets _ in _ tel (L2GMu) [notation, in GMu.Notations]
new _ [| _ , .. , _ |] ( _ ) (L2GMu) [notation, in GMu.Notations]
new _ [| |] ( _ ) (L2GMu) [notation, in GMu.Notations]
snd( _ ) (L2GMu) [notation, in GMu.Notations]
## _ (L2GMu) [notation, in GMu.Notations]
# _ (L2GMu) [notation, in GMu.Notations]
< _ , _ > (L2GMu) [notation, in GMu.Notations]
<.> (L2GMu) [notation, in GMu.Notations]
Λ => _ (L2GMu) [notation, in GMu.Notations]
γ( _ , .. , _ ) _ (L2GMu) [notation, in GMu.Notations]
γ() _ (L2GMu) [notation, in GMu.Notations]
λ _ => _ (L2GMu) [notation, in GMu.Notations]
∀ _ (L2GMu) [notation, in GMu.Notations]
_ --> _ [notation, in GMu.Definitions]
_ ≡ _ [notation, in GMu.Definitions]
_ ~l _ [notation, in GMu.Definitions]
_ ~f _ [notation, in GMu.Definitions]
_ open_ee_varfix _ [notation, in GMu.Definitions]
_ open_ee_varlam _ [notation, in GMu.Definitions]
_ open_te_var _ [notation, in GMu.Definitions]
_ open_tt_var _ [notation, in GMu.Definitions]
_ ** _ [notation, in GMu.Definitions]
_ ==> _ [notation, in GMu.Definitions]
_ |, _ [notation, in GMu.Definitions]
_ |,| _ [notation, in GMu.Definitions]
{ _ , _ , _ } ⊢( _ ) _ ∈ _ [notation, in GMu.Definitions]
Δ1:120 [binder, in GMu.Preservation]
Δ1:128 [binder, in GMu.SubstMatch]
Δ1:144 [binder, in GMu.SubstMatch]
Δ1:158 [binder, in GMu.SubstMatch]
Δ1:171 [binder, in GMu.SubstMatch]
Δ1:178 [binder, in GMu.Preservation]
Δ1:184 [binder, in GMu.SubstMatch]
Δ1:191 [binder, in GMu.SubstMatch]
Δ1:197 [binder, in GMu.SubstMatch]
Δ1:236 [binder, in GMu.SubstMatch]
Δ1:243 [binder, in GMu.SubstMatch]
Δ2:121 [binder, in GMu.Preservation]
Δ2:141 [binder, in GMu.Preservation]
Δ2:179 [binder, in GMu.Preservation]
Δ2:185 [binder, in GMu.SubstMatch]
Δ2:192 [binder, in GMu.SubstMatch]
Δ2:198 [binder, in GMu.SubstMatch]
Δ2:237 [binder, in GMu.SubstMatch]
Δ2:244 [binder, in GMu.SubstMatch]
Δ:101 [binder, in GMu.Regularity]
Δ:104 [binder, in GMu.SubstMatch]
Δ:104 [binder, in GMu.Regularity]
Δ:109 [binder, in GMu.SubstMatch]
Δ:11 [binder, in GMu.CanonicalForms]
Δ:114 [binder, in GMu.Regularity]
Δ:115 [binder, in GMu.SubstMatch]
Δ:118 [binder, in GMu.Regularity]
Δ:12 [binder, in GMu.Equations]
Δ:120 [binder, in GMu.SubstMatch]
Δ:122 [binder, in GMu.SubstMatch]
Δ:126 [binder, in GMu.InfrastructureFV]
Δ:128 [binder, in GMu.Regularity]
Δ:131 [binder, in GMu.Preservation]
Δ:134 [binder, in GMu.Regularity]
Δ:138 [binder, in GMu.InfrastructureFV]
Δ:140 [binder, in GMu.Preservation]
Δ:157 [binder, in GMu.Preservation]
Δ:16 [binder, in GMu.Equations]
Δ:168 [binder, in GMu.Preservation]
Δ:18 [binder, in GMu.Preservation]
Δ:182 [binder, in GMu.SubstMatch]
Δ:182 [binder, in GMu.InfrastructureFV]
Δ:186 [binder, in GMu.InfrastructureFV]
Δ:187 [binder, in GMu.Preservation]
Δ:2 [binder, in GMu.Equations]
Δ:2 [binder, in GMu.CanonicalForms]
Δ:20 [binder, in GMu.CanonicalForms]
Δ:208 [binder, in GMu.SubstMatch]
Δ:215 [binder, in GMu.SubstMatch]
Δ:27 [binder, in GMu.CanonicalForms]
Δ:27 [binder, in GMu.Preservation]
Δ:27 [binder, in GMu.TestCommon]
Δ:285 [binder, in GMu.Definitions]
Δ:287 [binder, in GMu.Definitions]
Δ:290 [binder, in GMu.Definitions]
Δ:299 [binder, in GMu.Definitions]
Δ:301 [binder, in GMu.Definitions]
Δ:304 [binder, in GMu.Definitions]
Δ:308 [binder, in GMu.Definitions]
Δ:313 [binder, in GMu.Definitions]
Δ:317 [binder, in GMu.Definitions]
Δ:32 [binder, in GMu.Equations]
Δ:33 [binder, in GMu.CanonicalForms]
Δ:331 [binder, in GMu.Definitions]
Δ:335 [binder, in GMu.Definitions]
Δ:339 [binder, in GMu.Definitions]
Δ:34 [binder, in GMu.TestCommon]
Δ:345 [binder, in GMu.Definitions]
Δ:357 [binder, in GMu.Definitions]
Δ:36 [binder, in GMu.Regularity]
Δ:36 [binder, in GMu.Preservation]
Δ:361 [binder, in GMu.Definitions]
Δ:37 [binder, in GMu.Equations]
Δ:373 [binder, in GMu.Definitions]
Δ:375 [binder, in GMu.Definitions]
Δ:38 [binder, in GMu.CanonicalForms]
Δ:389 [binder, in GMu.Definitions]
Δ:393 [binder, in GMu.Definitions]
Δ:399 [binder, in GMu.Definitions]
Δ:4 [binder, in GMu.Equations]
Δ:40 [binder, in GMu.Regularity]
Δ:41 [binder, in GMu.CanonicalForms]
Δ:415 [binder, in GMu.Definitions]
Δ:423 [binder, in GMu.Definitions]
Δ:43 [binder, in GMu.Regularity]
Δ:433 [binder, in GMu.Definitions]
Δ:441 [binder, in GMu.Definitions]
Δ:449 [binder, in GMu.Definitions]
Δ:45 [binder, in GMu.Equations]
Δ:458 [binder, in GMu.Definitions]
Δ:46 [binder, in GMu.Preservation]
Δ:465 [binder, in GMu.Definitions]
Δ:47 [binder, in GMu.Regularity2]
Δ:473 [binder, in GMu.Definitions]
Δ:482 [binder, in GMu.Definitions]
Δ:49 [binder, in GMu.Regularity]
Δ:493 [binder, in GMu.Definitions]
Δ:5 [binder, in GMu.Regularity]
Δ:512 [binder, in GMu.Definitions]
Δ:52 [binder, in GMu.Equations]
Δ:53 [binder, in GMu.Regularity2]
Δ:55 [binder, in GMu.Regularity]
Δ:59 [binder, in GMu.Equations]
Δ:66 [binder, in GMu.Equations]
Δ:67 [binder, in GMu.Regularity]
Δ:7 [binder, in GMu.Equations]
Δ:71 [binder, in GMu.Regularity2]
Δ:72 [binder, in GMu.Equations]
Δ:73 [binder, in GMu.Regularity]
Δ:78 [binder, in GMu.Equations]
Δ:8 [binder, in GMu.Regularity]
Δ:84 [binder, in GMu.Equations]
Δ:87 [binder, in GMu.Regularity]
Δ:88 [binder, in GMu.Equations]
Δ:94 [binder, in GMu.SubstMatch]
Δ:95 [binder, in GMu.Preservation]
Θ1:15 [binder, in GMu.SubstMatch]
Θ1:54 [binder, in GMu.SubstMatch]
Θ1:63 [binder, in GMu.SubstMatch]
Θ1:72 [binder, in GMu.SubstMatch]
Θ2:16 [binder, in GMu.SubstMatch]
Θ2:55 [binder, in GMu.SubstMatch]
Θ2:64 [binder, in GMu.SubstMatch]
Θ2:73 [binder, in GMu.SubstMatch]
Θ:1 [binder, in GMu.InfrastructureSubstPrim]
Θ:13 [binder, in GMu.Equations]
Θ:14 [binder, in GMu.SubstMatch]
Θ:276 [binder, in GMu.Definitions]
Θ:3 [binder, in GMu.SubstMatch]
Θ:3 [binder, in GMu.InfrastructureSubstPrim]
Θ:31 [binder, in GMu.Equations]
Θ:324 [binder, in GMu.Definitions]
Θ:330 [binder, in GMu.Definitions]
Θ:334 [binder, in GMu.Definitions]
Θ:342 [binder, in GMu.Definitions]
Θ:38 [binder, in GMu.Equations]
Θ:41 [binder, in GMu.Equations]
Θ:47 [binder, in GMu.SubstMatch]
Θ:5 [binder, in GMu.SubstMatch]
Θ:67 [binder, in GMu.Equations]
Σ:1 [binder, in GMu.Regularity2]
Σ:1 [binder, in GMu.SubstMatch]
Σ:1 [binder, in GMu.Regularity]
Σ:1 [binder, in GMu.CanonicalForms]
Σ:1 [binder, in GMu.Tests]
Σ:10 [binder, in GMu.SubstMatch]
Σ:10 [binder, in GMu.CanonicalForms]
Σ:10 [binder, in GMu.Preservation]
Σ:101 [binder, in GMu.Equations]
Σ:102 [binder, in GMu.SubstMatch]
Σ:105 [binder, in GMu.Regularity]
Σ:107 [binder, in GMu.SubstMatch]
Σ:11 [binder, in GMu.Equations]
Σ:112 [binder, in GMu.SubstMatch]
Σ:113 [binder, in GMu.Regularity]
Σ:117 [binder, in GMu.SubstMatch]
Σ:117 [binder, in GMu.Regularity]
Σ:119 [binder, in GMu.Preservation]
Σ:121 [binder, in GMu.SubstMatch]
Σ:127 [binder, in GMu.SubstMatch]
Σ:127 [binder, in GMu.Regularity]
Σ:13 [binder, in GMu.Regularity]
Σ:130 [binder, in GMu.Preservation]
Σ:133 [binder, in GMu.Regularity]
Σ:137 [binder, in GMu.InfrastructureFV]
Σ:139 [binder, in GMu.Preservation]
Σ:14 [binder, in GMu.Regularity2]
Σ:143 [binder, in GMu.SubstMatch]
Σ:156 [binder, in GMu.Preservation]
Σ:157 [binder, in GMu.SubstMatch]
Σ:167 [binder, in GMu.Preservation]
Σ:17 [binder, in GMu.Preservation]
Σ:170 [binder, in GMu.SubstMatch]
Σ:177 [binder, in GMu.Preservation]
Σ:18 [binder, in GMu.SubstMatch]
Σ:180 [binder, in GMu.SubstMatch]
Σ:183 [binder, in GMu.SubstMatch]
Σ:186 [binder, in GMu.Preservation]
Σ:19 [binder, in GMu.Regularity2]
Σ:19 [binder, in GMu.CanonicalForms]
Σ:190 [binder, in GMu.SubstMatch]
Σ:196 [binder, in GMu.SubstMatch]
Σ:2 [binder, in GMu.Preservation]
Σ:207 [binder, in GMu.SubstMatch]
Σ:214 [binder, in GMu.SubstMatch]
Σ:22 [binder, in GMu.Regularity]
Σ:229 [binder, in GMu.SubstMatch]
Σ:23 [binder, in GMu.SubstMatch]
Σ:235 [binder, in GMu.SubstMatch]
Σ:242 [binder, in GMu.SubstMatch]
Σ:26 [binder, in GMu.Regularity2]
Σ:26 [binder, in GMu.CanonicalForms]
Σ:26 [binder, in GMu.Preservation]
Σ:26 [binder, in GMu.TestCommon]
Σ:27 [binder, in GMu.Regularity]
Σ:29 [binder, in GMu.Equations]
Σ:298 [binder, in GMu.Definitions]
Σ:300 [binder, in GMu.Definitions]
Σ:303 [binder, in GMu.Definitions]
Σ:307 [binder, in GMu.Definitions]
Σ:312 [binder, in GMu.Definitions]
Σ:316 [binder, in GMu.Definitions]
Σ:32 [binder, in GMu.CanonicalForms]
Σ:327 [binder, in GMu.Definitions]
Σ:33 [binder, in GMu.TestCommon]
Σ:338 [binder, in GMu.Definitions]
Σ:34 [binder, in GMu.Regularity2]
Σ:34 [binder, in GMu.SubstMatch]
Σ:34 [binder, in GMu.Regularity]
Σ:344 [binder, in GMu.Definitions]
Σ:35 [binder, in GMu.Preservation]
Σ:353 [binder, in GMu.Definitions]
Σ:36 [binder, in GMu.Equations]
Σ:365 [binder, in GMu.Definitions]
Σ:37 [binder, in GMu.CanonicalForms]
Σ:372 [binder, in GMu.Definitions]
Σ:374 [binder, in GMu.Definitions]
Σ:388 [binder, in GMu.Definitions]
Σ:39 [binder, in GMu.Regularity]
Σ:391 [binder, in GMu.Definitions]
Σ:397 [binder, in GMu.Definitions]
Σ:4 [binder, in GMu.SubstMatch]
Σ:4 [binder, in GMu.Regularity]
Σ:40 [binder, in GMu.Regularity2]
Σ:40 [binder, in GMu.SubstMatch]
Σ:40 [binder, in GMu.CanonicalForms]
Σ:414 [binder, in GMu.Definitions]
Σ:42 [binder, in GMu.Regularity]
Σ:422 [binder, in GMu.Definitions]
Σ:432 [binder, in GMu.Definitions]
Σ:44 [binder, in GMu.Equations]
Σ:440 [binder, in GMu.Definitions]
Σ:448 [binder, in GMu.Definitions]
Σ:45 [binder, in GMu.Preservation]
Σ:457 [binder, in GMu.Definitions]
Σ:46 [binder, in GMu.Regularity2]
Σ:464 [binder, in GMu.Definitions]
Σ:472 [binder, in GMu.Definitions]
Σ:48 [binder, in GMu.Regularity]
Σ:481 [binder, in GMu.Definitions]
Σ:492 [binder, in GMu.Definitions]
Σ:5 [binder, in GMu.Regularity2]
Σ:50 [binder, in GMu.Equations]
Σ:51 [binder, in GMu.Equations]
Σ:511 [binder, in GMu.Definitions]
Σ:52 [binder, in GMu.Regularity2]
Σ:54 [binder, in GMu.Regularity]
Σ:58 [binder, in GMu.SubstMatch]
Σ:58 [binder, in GMu.Equations]
Σ:584 [binder, in GMu.Definitions]
Σ:589 [binder, in GMu.Definitions]
Σ:61 [binder, in GMu.Regularity]
Σ:64 [binder, in GMu.Regularity2]
Σ:65 [binder, in GMu.Equations]
Σ:66 [binder, in GMu.Regularity]
Σ:7 [binder, in GMu.Regularity]
Σ:70 [binder, in GMu.Regularity2]
Σ:71 [binder, in GMu.SubstMatch]
Σ:71 [binder, in GMu.Equations]
Σ:72 [binder, in GMu.Regularity]
Σ:75 [binder, in GMu.Regularity]
Σ:77 [binder, in GMu.Equations]
Σ:78 [binder, in GMu.Regularity2]
Σ:78 [binder, in GMu.SubstMatch]
Σ:80 [binder, in GMu.Regularity]
Σ:83 [binder, in GMu.Equations]
Σ:84 [binder, in GMu.SubstMatch]
Σ:86 [binder, in GMu.Regularity]
Σ:87 [binder, in GMu.Equations]
Σ:9 [binder, in GMu.Regularity2]
Σ:90 [binder, in GMu.Regularity]
Σ:92 [binder, in GMu.SubstMatch]
Σ:94 [binder, in GMu.Preservation]
Σ:98 [binder, in GMu.Regularity]
ϵ:142 [binder, in GMu.InfrastructureFV]
ϵ:171 [binder, in GMu.Prelude]
ϵ:25 [binder, in GMu.Regularity2]
ϵ:25 [binder, in GMu.Regularity]
ϵ:25 [binder, in GMu.Preservation]
ϵ:33 [binder, in GMu.Regularity]

---

Notation Index

other

case_pattern:_ => _ (L2GMu) [in GMu.Notations]
[ _ ; _ ; .. ; _ ]* (list_scope) [in GMu.Definitions]
[ _ ]* (list_scope) [in GMu.Definitions]
[ ]* (list_scope) [in GMu.Definitions]
_ <|| _ (L2GMu) [in GMu.Notations]
_ <| _ (L2GMu) [in GMu.Notations]
_ ==> _ (L2GMu) [in GMu.Notations]
_ ** _ (L2GMu) [in GMu.Notations]
case _ as _ of { _ | .. | _ } (L2GMu) [in GMu.Notations]
enum _ {{ _ | .. | _ }} (L2GMu) [in GMu.Notations]
fixs _ => _ (L2GMu) [in GMu.Notations]
fst( _ ) (L2GMu) [in GMu.Notations]
lets _ in _ tel (L2GMu) [in GMu.Notations]
new _ [| _ , .. , _ |] ( _ ) (L2GMu) [in GMu.Notations]
new _ [| |] ( _ ) (L2GMu) [in GMu.Notations]
snd( _ ) (L2GMu) [in GMu.Notations]
## _ (L2GMu) [in GMu.Notations]
# _ (L2GMu) [in GMu.Notations]
< _ , _ > (L2GMu) [in GMu.Notations]
<.> (L2GMu) [in GMu.Notations]
Λ => _ (L2GMu) [in GMu.Notations]
γ( _ , .. , _ ) _ (L2GMu) [in GMu.Notations]
γ() _ (L2GMu) [in GMu.Notations]
λ _ => _ (L2GMu) [in GMu.Notations]
∀ _ (L2GMu) [in GMu.Notations]
_ --> _ [in GMu.Definitions]
_ ≡ _ [in GMu.Definitions]
_ ~l _ [in GMu.Definitions]
_ ~f _ [in GMu.Definitions]
_ open_ee_varfix _ [in GMu.Definitions]
_ open_ee_varlam _ [in GMu.Definitions]
_ open_te_var _ [in GMu.Definitions]
_ open_tt_var _ [in GMu.Definitions]
_ ** _ [in GMu.Definitions]
_ ==> _ [in GMu.Definitions]
_ |, _ [in GMu.Definitions]
_ |,| _ [in GMu.Definitions]
{ _ , _ , _ } ⊢( _ ) _ ∈ _ [in GMu.Definitions]

---

Binder Index

A

acc:149 [in GMu.Prelude]
acc:151 [in GMu.Prelude]
acc:153 [in GMu.Prelude]
acc:155 [in GMu.Prelude]
acc:20 [in GMu.Equations]
acc:22 [in GMu.Equations]
acc:24 [in GMu.Equations]
acc:26 [in GMu.Equations]
acc:295 [in GMu.Definitions]
Ah:132 [in GMu.Prelude]
Alphas:106 [in GMu.Regularity]
Alphas:227 [in GMu.Definitions]
Alphas:355 [in GMu.Definitions]
Alphas:359 [in GMu.Definitions]
Alphas:508 [in GMu.Definitions]
Alphas:75 [in GMu.Prelude]
alpha:358 [in GMu.Definitions]
alpha:362 [in GMu.Definitions]
args:143 [in GMu.Definitions]
args:147 [in GMu.Definitions]
args:151 [in GMu.Definitions]
args:153 [in GMu.Definitions]
argT:352 [in GMu.Definitions]
Arity:320 [in GMu.Definitions]
Arity:367 [in GMu.Definitions]
As:106 [in GMu.Zip]
As:112 [in GMu.Zip]
As:119 [in GMu.InfrastructureFV]
As:125 [in GMu.InfrastructureOpen]
As:137 [in GMu.InfrastructureOpen]
As:138 [in GMu.Preservation]
As:153 [in GMu.InfrastructureFV]
As:158 [in GMu.InfrastructureSubst]
As:162 [in GMu.InfrastructureSubst]
As:162 [in GMu.InfrastructureFV]
As:169 [in GMu.InfrastructureFV]
As:172 [in GMu.InfrastructureSubst]
As:176 [in GMu.InfrastructureSubst]
As:181 [in GMu.InfrastructureFV]
As:197 [in GMu.Preservation]
As:209 [in GMu.SubstMatch]
As:27 [in GMu.Equations]
As:272 [in GMu.Definitions]
As:29 [in GMu.Regularity2]
As:29 [in GMu.Preservation]
As:30 [in GMu.Equations]
As:34 [in GMu.Zip]
As:35 [in GMu.Regularity]
As:35 [in GMu.Equations]
As:41 [in GMu.Zip]
As:49 [in GMu.Zip]
As:56 [in GMu.Zip]
As:62 [in GMu.Zip]
As:69 [in GMu.InfrastructureFV]
As:70 [in GMu.Zip]
As:77 [in GMu.Zip]
As:83 [in GMu.Zip]
As:90 [in GMu.Zip]
As:93 [in GMu.InfrastructureOpen]
As:96 [in GMu.Prelude]
As:99 [in GMu.Regularity]
Ats:133 [in GMu.Prelude]
AT:102 [in GMu.Zip]
AT:108 [in GMu.Zip]
AT:47 [in GMu.Zip]
AT:54 [in GMu.Zip]
AT:60 [in GMu.Zip]
AT:68 [in GMu.Zip]
AT:75 [in GMu.Zip]
AT:81 [in GMu.Zip]
AT:88 [in GMu.Zip]
A:1 [in GMu.InfrastructureFV]
A:10 [in GMu.TestVector]
a:101 [in GMu.Zip]
A:104 [in GMu.Zip]
A:104 [in GMu.Definitions]
A:105 [in GMu.SubstMatch]
A:107 [in GMu.Prelude]
A:109 [in GMu.Regularity]
A:110 [in GMu.Zip]
A:110 [in GMu.SubstMatch]
A:110 [in GMu.Regularity]
A:112 [in GMu.Prelude]
A:117 [in GMu.Preservation]
a:118 [in GMu.Prelude]
A:118 [in GMu.Preservation]
a:120 [in GMu.Prelude]
A:122 [in GMu.Prelude]
A:125 [in GMu.Regularity]
A:126 [in GMu.Regularity]
A:129 [in GMu.Prelude]
A:138 [in GMu.Prelude]
A:14 [in GMu.TestCommon]
A:142 [in GMu.Prelude]
A:146 [in GMu.Prelude]
A:149 [in GMu.Preservation]
A:149 [in GMu.InfrastructureFV]
A:150 [in GMu.Preservation]
A:151 [in GMu.Preservation]
A:152 [in GMu.Preservation]
A:153 [in GMu.Preservation]
A:154 [in GMu.InfrastructureFV]
A:155 [in GMu.Preservation]
A:157 [in GMu.Prelude]
A:160 [in GMu.Prelude]
A:161 [in GMu.InfrastructureSubst]
a:165 [in GMu.Prelude]
A:167 [in GMu.InfrastructureSubst]
A:167 [in GMu.InfrastructureFV]
A:172 [in GMu.Prelude]
A:174 [in GMu.InfrastructureSubst]
A:176 [in GMu.Prelude]
A:177 [in GMu.InfrastructureFV]
A:178 [in GMu.InfrastructureSubst]
A:181 [in GMu.InfrastructureSubst]
A:183 [in GMu.Prelude]
A:19 [in GMu.TestCommon]
A:20 [in GMu.InfrastructureFV]
A:200 [in GMu.Preservation]
A:208 [in GMu.Preservation]
A:209 [in GMu.Preservation]
a:21 [in GMu.Zip]
A:229 [in GMu.Definitions]
A:233 [in GMu.SubstMatch]
a:25 [in GMu.Zip]
A:25 [in GMu.InfrastructureSubstPrim]
A:28 [in GMu.Equations]
A:283 [in GMu.Definitions]
a:29 [in GMu.Zip]
a:3 [in GMu.TestCommon]
A:30 [in GMu.InfrastructureSubst]
A:31 [in GMu.Regularity2]
A:32 [in GMu.Regularity2]
A:33 [in GMu.Regularity2]
A:33 [in GMu.Preservation]
A:332 [in GMu.Definitions]
A:34 [in GMu.Equations]
A:34 [in GMu.Preservation]
A:35 [in GMu.TestCommon]
A:36 [in GMu.InfrastructureSubst]
A:37 [in GMu.Zip]
A:38 [in GMu.Regularity]
A:39 [in GMu.Equations]
A:4 [in GMu.InfrastructureSubstPrim]
A:42 [in GMu.Equations]
A:42 [in GMu.InfrastructureFV]
A:43 [in GMu.Preservation]
a:44 [in GMu.Zip]
A:44 [in GMu.Prelude]
A:44 [in GMu.Preservation]
A:46 [in GMu.Zip]
A:46 [in GMu.Equations]
A:48 [in GMu.Prelude]
A:5 [in GMu.TestVector]
A:510 [in GMu.Definitions]
A:52 [in GMu.Zip]
A:52 [in GMu.SubstMatch]
a:53 [in GMu.Prelude]
A:55 [in GMu.Prelude]
A:575 [in GMu.Definitions]
A:58 [in GMu.Zip]
A:6 [in GMu.TestVector]
a:6 [in GMu.TestCommon]
a:63 [in GMu.Prelude]
a:65 [in GMu.Prelude]
A:66 [in GMu.Zip]
A:67 [in GMu.Prelude]
A:69 [in GMu.SubstMatch]
A:69 [in GMu.Equations]
A:7 [in GMu.TestCommon]
A:70 [in GMu.Prelude]
A:72 [in GMu.Zip]
A:76 [in GMu.Prelude]
A:77 [in GMu.Prelude]
a:78 [in GMu.Prelude]
A:79 [in GMu.Zip]
A:79 [in GMu.Prelude]
A:80 [in GMu.Preservation]
A:81 [in GMu.Preservation]
A:85 [in GMu.Zip]
A:92 [in GMu.Zip]
A:93 [in GMu.Prelude]
A:96 [in GMu.Zip]
A:98 [in GMu.Prelude]
A:99 [in GMu.SubstMatch]
A:99 [in GMu.Prelude]

B

base:10 [in GMu.InfrastructureFV]
base:15 [in GMu.InfrastructureFV]
base:25 [in GMu.InfrastructureFV]
base:31 [in GMu.InfrastructureFV]
base:39 [in GMu.InfrastructureFV]
base:5 [in GMu.InfrastructureFV]
Bs:107 [in GMu.Zip]
Bs:113 [in GMu.Zip]
Bs:35 [in GMu.Zip]
Bs:42 [in GMu.Zip]
Bs:50 [in GMu.Zip]
Bs:57 [in GMu.Zip]
Bs:63 [in GMu.Zip]
Bs:71 [in GMu.Zip]
Bs:78 [in GMu.Zip]
Bs:84 [in GMu.Zip]
Bs:91 [in GMu.Zip]
BT:103 [in GMu.Zip]
BT:109 [in GMu.Zip]
BT:48 [in GMu.Zip]
BT:55 [in GMu.Zip]
BT:61 [in GMu.Zip]
BT:69 [in GMu.Zip]
BT:76 [in GMu.Zip]
BT:82 [in GMu.Zip]
BT:89 [in GMu.Zip]
b:100 [in GMu.Zip]
B:100 [in GMu.SubstMatch]
B:100 [in GMu.Prelude]
B:105 [in GMu.Zip]
B:111 [in GMu.Zip]
B:113 [in GMu.Prelude]
b:119 [in GMu.Prelude]
b:121 [in GMu.Prelude]
B:139 [in GMu.Prelude]
B:143 [in GMu.Prelude]
B:147 [in GMu.Prelude]
B:158 [in GMu.Prelude]
B:161 [in GMu.Prelude]
B:163 [in GMu.InfrastructureFV]
b:166 [in GMu.Prelude]
B:170 [in GMu.InfrastructureFV]
B:177 [in GMu.Prelude]
B:20 [in GMu.TestCommon]
b:22 [in GMu.Zip]
b:26 [in GMu.Zip]
b:266 [in GMu.Definitions]
b:274 [in GMu.Definitions]
b:30 [in GMu.Zip]
B:36 [in GMu.Zip]
B:36 [in GMu.TestCommon]
b:4 [in GMu.TestCommon]
B:40 [in GMu.Equations]
B:43 [in GMu.Zip]
B:43 [in GMu.Equations]
B:43 [in GMu.InfrastructureFV]
b:45 [in GMu.Zip]
B:47 [in GMu.Equations]
B:49 [in GMu.Prelude]
B:53 [in GMu.Zip]
B:56 [in GMu.Prelude]
B:58 [in GMu.Prelude]
B:59 [in GMu.Zip]
b:64 [in GMu.Prelude]
B:65 [in GMu.Zip]
b:66 [in GMu.Prelude]
B:73 [in GMu.Zip]
B:8 [in GMu.TestCommon]
B:80 [in GMu.Zip]
B:80 [in GMu.Prelude]
B:86 [in GMu.Zip]
B:93 [in GMu.Zip]
B:94 [in GMu.Prelude]
B:97 [in GMu.Zip]

C

CargType:408 [in GMu.Definitions]
CargType:96 [in GMu.Regularity]
Carity:351 [in GMu.Definitions]
Carity:407 [in GMu.Definitions]
Carity:542 [in GMu.Definitions]
Carity:95 [in GMu.Regularity]
Ce:543 [in GMu.Definitions]
cid:539 [in GMu.Definitions]
clArity:39 [in GMu.Definitions]
Clauses:186 [in GMu.Prelude]
clauses:77 [in GMu.Definitions]
clauses:87 [in GMu.Definitions]
clause:4 [in GMu.Progress]
clause:505 [in GMu.Definitions]
clause:507 [in GMu.Definitions]
clause:6 [in GMu.Progress]
clA:189 [in GMu.Prelude]
clT:190 [in GMu.Prelude]
cl:17 [in GMu.InfrastructureFV]
cl:18 [in GMu.InfrastructureFV]
cl:188 [in GMu.Prelude]
cl:19 [in GMu.InfrastructureFV]
cl:226 [in GMu.Definitions]
cl:29 [in GMu.InfrastructureFV]
cl:33 [in GMu.InfrastructureFV]
cl:34 [in GMu.InfrastructureFV]
cl:35 [in GMu.InfrastructureFV]
cl:83 [in GMu.InfrastructureOpen]
CretTypes:409 [in GMu.Definitions]
CretTypes:97 [in GMu.Regularity]
cs:106 [in GMu.Definitions]
cs:109 [in GMu.Definitions]
Ctors:406 [in GMu.Definitions]
Ctors:93 [in GMu.Regularity]
Ctor:14 [in GMu.CanonicalForms]
Ctor:403 [in GMu.Definitions]
Ctor:549 [in GMu.Definitions]
Ctor:6 [in GMu.CanonicalForms]
Ctor:94 [in GMu.Regularity]
c:101 [in GMu.SubstMatch]
C:101 [in GMu.Prelude]
c:107 [in GMu.Definitions]
c:110 [in GMu.Definitions]
c:128 [in GMu.Definitions]
C:133 [in GMu.InfrastructureFV]
c:135 [in GMu.Definitions]
C:140 [in GMu.Prelude]
C:159 [in GMu.Prelude]
C:16 [in GMu.Zip]
c:171 [in GMu.Definitions]
C:37 [in GMu.TestCommon]
c:41 [in GMu.Definitions]
c:43 [in GMu.Definitions]
C:46 [in GMu.CanonicalForms]
C:48 [in GMu.Equations]
c:5 [in GMu.TestCommon]
C:57 [in GMu.Prelude]
c:80 [in GMu.Definitions]
C:81 [in GMu.Prelude]
c:88 [in GMu.Definitions]
C:9 [in GMu.Zip]
c:9 [in GMu.TestCommon]
c:91 [in GMu.Definitions]
c:92 [in GMu.Definitions]
c:94 [in GMu.Definitions]
C:95 [in GMu.Prelude]

D

Defs:185 [in GMu.Prelude]
Defs:321 [in GMu.Definitions]
Defs:368 [in GMu.Definitions]
Defs:502 [in GMu.Definitions]
def:187 [in GMu.Prelude]
def:3 [in GMu.Progress]
Def:369 [in GMu.Definitions]
def:5 [in GMu.Progress]
def:504 [in GMu.Definitions]
def:506 [in GMu.Definitions]
Deqs:140 [in GMu.InfrastructureFV]
Deqs:20 [in GMu.Preservation]
Deqs:22 [in GMu.Regularity2]
Deqs:29 [in GMu.Regularity]
D':89 [in GMu.SubstMatch]
D1:10 [in GMu.Regularity2]
D1:11 [in GMu.SubstMatch]
D1:11 [in GMu.Preservation]
D1:14 [in GMu.Regularity]
D1:15 [in GMu.Regularity2]
D1:151 [in GMu.InfrastructureFV]
D1:173 [in GMu.InfrastructureFV]
D1:20 [in GMu.Regularity2]
D1:23 [in GMu.Regularity]
D1:230 [in GMu.SubstMatch]
D1:24 [in GMu.SubstMatch]
D1:27 [in GMu.Regularity2]
D1:28 [in GMu.Regularity]
D1:3 [in GMu.Preservation]
D1:35 [in GMu.Regularity2]
D1:35 [in GMu.SubstMatch]
D1:41 [in GMu.Regularity2]
D1:41 [in GMu.SubstMatch]
D1:59 [in GMu.SubstMatch]
D1:6 [in GMu.Regularity2]
D1:6 [in GMu.SubstMatch]
D1:62 [in GMu.Regularity]
D1:65 [in GMu.Regularity2]
D1:74 [in GMu.SubstMatch]
D1:76 [in GMu.Regularity]
D1:79 [in GMu.Regularity2]
D1:79 [in GMu.SubstMatch]
D1:81 [in GMu.Regularity]
D1:92 [in GMu.InfrastructureFV]
D1:95 [in GMu.InfrastructureFV]
D2:11 [in GMu.Regularity2]
D2:116 [in GMu.SubstMatch]
D2:12 [in GMu.SubstMatch]
D2:12 [in GMu.Preservation]
D2:15 [in GMu.Regularity]
D2:152 [in GMu.InfrastructureFV]
D2:16 [in GMu.Regularity2]
D2:174 [in GMu.InfrastructureFV]
D2:21 [in GMu.Regularity2]
D2:232 [in GMu.SubstMatch]
D2:24 [in GMu.Regularity]
D2:26 [in GMu.SubstMatch]
D2:28 [in GMu.Regularity2]
D2:30 [in GMu.Regularity]
D2:36 [in GMu.Regularity2]
D2:37 [in GMu.SubstMatch]
D2:4 [in GMu.Preservation]
D2:42 [in GMu.Regularity2]
D2:42 [in GMu.SubstMatch]
D2:60 [in GMu.SubstMatch]
D2:63 [in GMu.Regularity]
D2:66 [in GMu.Regularity2]
D2:7 [in GMu.Regularity2]
D2:7 [in GMu.SubstMatch]
D2:75 [in GMu.SubstMatch]
D2:77 [in GMu.Regularity]
D2:80 [in GMu.Regularity2]
D2:80 [in GMu.SubstMatch]
D2:82 [in GMu.Regularity]
D2:93 [in GMu.InfrastructureFV]
D2:96 [in GMu.InfrastructureFV]
D3:32 [in GMu.SubstMatch]
D3:78 [in GMu.Regularity]
D4:33 [in GMu.SubstMatch]
D:167 [in GMu.Prelude]
d:181 [in GMu.Prelude]
D:19 [in GMu.SubstMatch]
D:2 [in GMu.Regularity2]
D:2 [in GMu.SubstMatch]
D:224 [in GMu.SubstMatch]
D:38 [in GMu.TestCommon]
D:49 [in GMu.Equations]
d:577 [in GMu.Definitions]
d:581 [in GMu.Definitions]
D:85 [in GMu.SubstMatch]
D:90 [in GMu.SubstMatch]

E

eq:141 [in GMu.InfrastructureFV]
eq:170 [in GMu.Prelude]
eq:18 [in GMu.Regularity2]
eq:24 [in GMu.Regularity2]
eq:24 [in GMu.Preservation]
eq:284 [in GMu.Definitions]
eq:32 [in GMu.Regularity]
eq:340 [in GMu.Definitions]
eq:7 [in GMu.Preservation]
eq:82 [in GMu.Regularity2]
e':27 [in GMu.InfrastructureFV]
e':5 [in GMu.Tests]
e':523 [in GMu.Definitions]
e':526 [in GMu.Definitions]
e':529 [in GMu.Definitions]
e':536 [in GMu.Definitions]
e':544 [in GMu.Definitions]
e':551 [in GMu.Definitions]
e':559 [in GMu.Definitions]
e':561 [in GMu.Definitions]
e':587 [in GMu.Definitions]
e':592 [in GMu.Definitions]
E0:106 [in GMu.Preservation]
E0:112 [in GMu.Preservation]
E0:57 [in GMu.Preservation]
E0:63 [in GMu.Preservation]
E0:69 [in GMu.Preservation]
E0:75 [in GMu.Preservation]
E0:83 [in GMu.Preservation]
E0:89 [in GMu.Preservation]
e1':546 [in GMu.Definitions]
e1':556 [in GMu.Definitions]
e1':564 [in GMu.Definitions]
e1':570 [in GMu.Definitions]
e1':574 [in GMu.Definitions]
e1:115 [in GMu.InfrastructureSubst]
e1:119 [in GMu.InfrastructureSubst]
e1:15 [in GMu.CanonicalForms]
e1:184 [in GMu.InfrastructureSubst]
e1:187 [in GMu.InfrastructureSubst]
e1:195 [in GMu.Definitions]
e1:197 [in GMu.Definitions]
e1:199 [in GMu.Definitions]
e1:200 [in GMu.Definitions]
e1:203 [in GMu.Definitions]
e1:205 [in GMu.Definitions]
e1:208 [in GMu.Definitions]
e1:219 [in GMu.Definitions]
e1:223 [in GMu.Definitions]
e1:231 [in GMu.Definitions]
e1:232 [in GMu.Definitions]
e1:234 [in GMu.Definitions]
e1:238 [in GMu.Definitions]
e1:404 [in GMu.Definitions]
e1:418 [in GMu.Definitions]
e1:427 [in GMu.Definitions]
e1:435 [in GMu.Definitions]
e1:443 [in GMu.Definitions]
e1:453 [in GMu.Definitions]
e1:462 [in GMu.Definitions]
e1:469 [in GMu.Definitions]
e1:486 [in GMu.Definitions]
e1:521 [in GMu.Definitions]
e1:524 [in GMu.Definitions]
e1:537 [in GMu.Definitions]
e1:545 [in GMu.Definitions]
e1:55 [in GMu.InfrastructureOpen]
e1:555 [in GMu.Definitions]
e1:562 [in GMu.Definitions]
e1:568 [in GMu.Definitions]
e1:571 [in GMu.Definitions]
e1:61 [in GMu.InfrastructureOpen]
e1:7 [in GMu.CanonicalForms]
e1:72 [in GMu.InfrastructureOpen]
e2':554 [in GMu.Definitions]
e2':567 [in GMu.Definitions]
e2:117 [in GMu.InfrastructureSubst]
e2:121 [in GMu.InfrastructureSubst]
e2:186 [in GMu.InfrastructureSubst]
e2:189 [in GMu.InfrastructureSubst]
e2:198 [in GMu.Definitions]
e2:206 [in GMu.Definitions]
e2:220 [in GMu.Definitions]
e2:235 [in GMu.Definitions]
e2:428 [in GMu.Definitions]
e2:454 [in GMu.Definitions]
e2:487 [in GMu.Definitions]
e2:528 [in GMu.Definitions]
e2:547 [in GMu.Definitions]
e2:553 [in GMu.Definitions]
e2:56 [in GMu.InfrastructureOpen]
e2:563 [in GMu.Definitions]
e2:566 [in GMu.Definitions]
e2:569 [in GMu.Definitions]
e2:62 [in GMu.InfrastructureOpen]
e2:73 [in GMu.InfrastructureOpen]
e:1 [in GMu.Prelude]
e:1 [in GMu.InfrastructureOpen]
e:100 [in GMu.InfrastructureSubst]
e:101 [in GMu.Preservation]
E:102 [in GMu.Prelude]
e:102 [in GMu.InfrastructureOpen]
e:105 [in GMu.InfrastructureSubst]
e:109 [in GMu.InfrastructureSubst]
E:111 [in GMu.Prelude]
e:112 [in GMu.Definitions]
e:112 [in GMu.InfrastructureSubst]
e:112 [in GMu.InfrastructureOpen]
e:115 [in GMu.InfrastructureOpen]
E:118 [in GMu.InfrastructureFV]
E:119 [in GMu.Regularity]
E:12 [in GMu.Regularity2]
E:12 [in GMu.Regularity]
E:12 [in GMu.CanonicalForms]
e:120 [in GMu.Regularity]
e:120 [in GMu.InfrastructureOpen]
E:122 [in GMu.Preservation]
E:122 [in GMu.InfrastructureFV]
e:124 [in GMu.Preservation]
e:128 [in GMu.InfrastructureOpen]
E:129 [in GMu.Regularity]
E:13 [in GMu.Preservation]
e:130 [in GMu.Regularity]
e:130 [in GMu.InfrastructureOpen]
e:132 [in GMu.Definitions]
E:132 [in GMu.Preservation]
E:132 [in GMu.InfrastructureFV]
e:134 [in GMu.Preservation]
E:135 [in GMu.Regularity]
e:137 [in GMu.Regularity]
e:139 [in GMu.InfrastructureSubst]
e:142 [in GMu.InfrastructureSubst]
E:142 [in GMu.Preservation]
e:144 [in GMu.Preservation]
e:147 [in GMu.InfrastructureSubst]
e:148 [in GMu.Definitions]
e:152 [in GMu.InfrastructureSubst]
e:154 [in GMu.Definitions]
E:158 [in GMu.Preservation]
e:16 [in GMu.Prelude]
e:164 [in GMu.InfrastructureSubst]
e:164 [in GMu.Preservation]
e:167 [in GMu.Definitions]
E:168 [in GMu.InfrastructureSubst]
E:169 [in GMu.Preservation]
E:17 [in GMu.Regularity2]
e:17 [in GMu.Prelude]
e:174 [in GMu.Preservation]
E:175 [in GMu.InfrastructureSubst]
E:180 [in GMu.Preservation]
e:181 [in GMu.Preservation]
e:182 [in GMu.Prelude]
E:188 [in GMu.Preservation]
e:189 [in GMu.Preservation]
e:19 [in GMu.Prelude]
E:19 [in GMu.Preservation]
E:2 [in GMu.Regularity]
e:2 [in GMu.Tests]
e:21 [in GMu.Prelude]
e:21 [in GMu.CanonicalForms]
e:22 [in GMu.InfrastructureFV]
E:223 [in GMu.SubstMatch]
E:23 [in GMu.Regularity2]
e:23 [in GMu.Prelude]
e:255 [in GMu.Definitions]
e:26 [in GMu.Prelude]
e:261 [in GMu.Definitions]
e:27 [in GMu.Prelude]
e:28 [in GMu.Prelude]
e:28 [in GMu.CanonicalForms]
E:28 [in GMu.Preservation]
E:293 [in GMu.Definitions]
E:3 [in GMu.Regularity2]
E:3 [in GMu.CanonicalForms]
E:30 [in GMu.Regularity2]
e:31 [in GMu.Prelude]
e:32 [in GMu.Prelude]
e:34 [in GMu.Prelude]
e:34 [in GMu.CanonicalForms]
e:36 [in GMu.Prelude]
E:37 [in GMu.Preservation]
E:376 [in GMu.Definitions]
e:38 [in GMu.Prelude]
e:39 [in GMu.CanonicalForms]
E:390 [in GMu.Definitions]
E:392 [in GMu.Definitions]
E:398 [in GMu.Definitions]
e:40 [in GMu.Definitions]
e:40 [in GMu.Preservation]
E:41 [in GMu.Regularity]
E:416 [in GMu.Definitions]
e:42 [in GMu.CanonicalForms]
E:424 [in GMu.Definitions]
E:434 [in GMu.Definitions]
E:44 [in GMu.Regularity]
E:442 [in GMu.Definitions]
E:450 [in GMu.Definitions]
E:459 [in GMu.Definitions]
E:466 [in GMu.Definitions]
E:47 [in GMu.Preservation]
E:474 [in GMu.Definitions]
E:48 [in GMu.Regularity2]
e:48 [in GMu.InfrastructureFV]
E:483 [in GMu.Definitions]
E:494 [in GMu.Definitions]
e:495 [in GMu.Definitions]
E:5 [in GMu.Preservation]
e:5 [in GMu.InfrastructureOpen]
E:50 [in GMu.Regularity]
e:50 [in GMu.InfrastructureSubst]
e:50 [in GMu.InfrastructureFV]
e:51 [in GMu.Definitions]
e:51 [in GMu.InfrastructureSubst]
e:51 [in GMu.InfrastructureOpen]
E:513 [in GMu.Definitions]
e:516 [in GMu.Definitions]
e:52 [in GMu.Preservation]
E:53 [in GMu.Equations]
e:53 [in GMu.InfrastructureOpen]
E:54 [in GMu.Regularity2]
e:54 [in GMu.Equations]
e:550 [in GMu.Definitions]
e:558 [in GMu.Definitions]
E:56 [in GMu.Regularity]
e:560 [in GMu.Definitions]
e:58 [in GMu.InfrastructureSubst]
e:58 [in GMu.InfrastructureOpen]
e:585 [in GMu.Definitions]
e:59 [in GMu.Definitions]
e:590 [in GMu.Definitions]
E:6 [in GMu.Regularity]
E:60 [in GMu.Equations]
e:61 [in GMu.Equations]
e:61 [in GMu.Definitions]
e:61 [in GMu.InfrastructureSubst]
E:64 [in GMu.Regularity]
e:64 [in GMu.Definitions]
e:64 [in GMu.InfrastructureOpen]
e:65 [in GMu.InfrastructureSubst]
e:66 [in GMu.InfrastructureOpen]
E:67 [in GMu.Regularity2]
E:68 [in GMu.Regularity]
e:69 [in GMu.Definitions]
e:69 [in GMu.InfrastructureOpen]
e:7 [in GMu.InfrastructureFV]
e:71 [in GMu.Definitions]
E:72 [in GMu.Regularity2]
e:74 [in GMu.Definitions]
e:75 [in GMu.InfrastructureFV]
e:76 [in GMu.InfrastructureSubst]
e:77 [in GMu.InfrastructureOpen]
e:79 [in GMu.Definitions]
E:8 [in GMu.Regularity2]
e:80 [in GMu.InfrastructureSubst]
e:80 [in GMu.InfrastructureOpen]
e:80 [in GMu.InfrastructureFV]
E:81 [in GMu.Regularity2]
E:83 [in GMu.InfrastructureFV]
e:84 [in GMu.InfrastructureOpen]
e:85 [in GMu.InfrastructureSubst]
E:87 [in GMu.InfrastructureFV]
e:88 [in GMu.InfrastructureOpen]
e:89 [in GMu.InfrastructureSubst]
E:96 [in GMu.Preservation]
e:96 [in GMu.InfrastructureOpen]
e:97 [in GMu.InfrastructureOpen]

F

fv:100 [in GMu.InfrastructureFV]
fv:108 [in GMu.InfrastructureFV]
fv:11 [in GMu.InfrastructureFV]
fv:135 [in GMu.InfrastructureFV]
fv:158 [in GMu.Definitions]
fv:16 [in GMu.InfrastructureFV]
fv:164 [in GMu.InfrastructureFV]
fv:165 [in GMu.Definitions]
fv:170 [in GMu.Definitions]
fv:171 [in GMu.InfrastructureFV]
fv:172 [in GMu.Definitions]
fv:26 [in GMu.InfrastructureFV]
fv:32 [in GMu.InfrastructureFV]
fv:40 [in GMu.InfrastructureFV]
fv:49 [in GMu.InfrastructureFV]
fv:6 [in GMu.InfrastructureFV]
F0:107 [in GMu.Preservation]
F0:113 [in GMu.Preservation]
F0:19 [in GMu.Regularity]
F0:21 [in GMu.Regularity]
F0:58 [in GMu.Preservation]
F0:64 [in GMu.Preservation]
F0:70 [in GMu.Preservation]
F0:76 [in GMu.Preservation]
F0:84 [in GMu.Preservation]
F0:90 [in GMu.Preservation]
F1:95 [in GMu.Equations]
F2:96 [in GMu.Equations]
f:10 [in GMu.Zip]
f:103 [in GMu.Prelude]
f:105 [in GMu.Definitions]
f:108 [in GMu.Definitions]
f:115 [in GMu.Prelude]
f:128 [in GMu.Prelude]
F:136 [in GMu.Prelude]
F:143 [in GMu.Preservation]
F:159 [in GMu.Preservation]
f:162 [in GMu.Prelude]
f:17 [in GMu.Zip]
F:178 [in GMu.Prelude]
F:184 [in GMu.Prelude]
f:21 [in GMu.TestCommon]
F:38 [in GMu.Preservation]
F:4 [in GMu.Regularity2]
f:45 [in GMu.Prelude]
F:48 [in GMu.Preservation]
f:50 [in GMu.Prelude]
F:55 [in GMu.Regularity2]
F:60 [in GMu.Regularity]
F:73 [in GMu.Regularity2]
f:82 [in GMu.Prelude]
F:94 [in GMu.Equations]
F:97 [in GMu.Preservation]
F:98 [in GMu.Zip]

G

GADTC:53 [in GMu.Definitions]
GTs:133 [in GMu.InfrastructureOpen]
g:104 [in GMu.Prelude]
g:116 [in GMu.Prelude]
G:224 [in GMu.Definitions]
G:39 [in GMu.Preservation]
g:51 [in GMu.Prelude]
G:538 [in GMu.Definitions]
G:572 [in GMu.Definitions]
G:78 [in GMu.Definitions]
G:79 [in GMu.InfrastructureOpen]
g:83 [in GMu.Prelude]

H

head_proof:93 [in GMu.Definitions]
h:105 [in GMu.Prelude]
h:3 [in GMu.Definitions]
h:8 [in GMu.TestVector]

I

i:119 [in GMu.InfrastructureOpen]
i:124 [in GMu.InfrastructureOpen]
i:45 [in GMu.InfrastructureOpen]
i:51 [in GMu.Zip]
i:64 [in GMu.Zip]
i:67 [in GMu.Zip]
i:74 [in GMu.Zip]
i:87 [in GMu.Zip]
i:94 [in GMu.Zip]
i:95 [in GMu.Zip]

J

j:116 [in GMu.InfrastructureOpen]
j:121 [in GMu.InfrastructureOpen]
J:15 [in GMu.InfrastructureOpen]

K

k:105 [in GMu.InfrastructureOpen]
k:108 [in GMu.InfrastructureSubst]
k:108 [in GMu.InfrastructureOpen]
k:111 [in GMu.InfrastructureOpen]
k:114 [in GMu.InfrastructureOpen]
k:115 [in GMu.Definitions]
k:118 [in GMu.InfrastructureSubst]
k:12 [in GMu.Prelude]
k:120 [in GMu.Definitions]
k:122 [in GMu.InfrastructureSubst]
k:123 [in GMu.Definitions]
k:126 [in GMu.InfrastructureOpen]
k:130 [in GMu.Definitions]
k:131 [in GMu.InfrastructureOpen]
k:16 [in GMu.InfrastructureOpen]
k:18 [in GMu.InfrastructureOpen]
k:19 [in GMu.InfrastructureOpen]
k:22 [in GMu.InfrastructureOpen]
k:25 [in GMu.InfrastructureOpen]
k:259 [in GMu.Definitions]
k:27 [in GMu.InfrastructureOpen]
k:30 [in GMu.InfrastructureOpen]
k:33 [in GMu.InfrastructureOpen]
k:39 [in GMu.InfrastructureOpen]
k:42 [in GMu.InfrastructureOpen]
k:46 [in GMu.InfrastructureOpen]
k:48 [in GMu.Definitions]
k:49 [in GMu.InfrastructureOpen]
k:50 [in GMu.InfrastructureOpen]
k:52 [in GMu.InfrastructureOpen]
k:53 [in GMu.InfrastructureFV]
k:54 [in GMu.InfrastructureOpen]
k:56 [in GMu.InfrastructureFV]
k:57 [in GMu.InfrastructureOpen]
k:59 [in GMu.InfrastructureFV]
k:60 [in GMu.InfrastructureOpen]
k:62 [in GMu.InfrastructureFV]
k:63 [in GMu.InfrastructureSubst]
k:63 [in GMu.InfrastructureOpen]
k:65 [in GMu.InfrastructureOpen]
k:68 [in GMu.InfrastructureOpen]
k:69 [in GMu.InfrastructureSubst]
k:71 [in GMu.InfrastructureOpen]
k:74 [in GMu.InfrastructureSubst]
k:74 [in GMu.InfrastructureOpen]
k:74 [in GMu.InfrastructureFV]
k:76 [in GMu.InfrastructureFV]
k:78 [in GMu.InfrastructureOpen]
k:82 [in GMu.InfrastructureOpen]
k:86 [in GMu.InfrastructureOpen]
k:87 [in GMu.InfrastructureSubst]
k:91 [in GMu.InfrastructureOpen]

L

la:11 [in GMu.Zip]
la:163 [in GMu.Prelude]
la:18 [in GMu.Zip]
la:23 [in GMu.Zip]
la:27 [in GMu.Zip]
la:4 [in GMu.Zip]
lb:12 [in GMu.Zip]
lb:164 [in GMu.Prelude]
lb:19 [in GMu.Zip]
lb:24 [in GMu.Zip]
lb:28 [in GMu.Zip]
lb:5 [in GMu.Zip]
len:74 [in GMu.Prelude]
list_clause_ind:96 [in GMu.Definitions]
list_typ_ind:31 [in GMu.Definitions]
LPt:30 [in GMu.Definitions]
ls:105 [in GMu.InfrastructureFV]
ls:114 [in GMu.Prelude]
ls:14 [in GMu.InfrastructureFV]
ls:21 [in GMu.Definitions]
ls:24 [in GMu.InfrastructureFV]
ls:26 [in GMu.Definitions]
ls:3 [in GMu.InfrastructureFV]
ls:30 [in GMu.InfrastructureFV]
ls:38 [in GMu.InfrastructureFV]
ls:44 [in GMu.InfrastructureFV]
ls:46 [in GMu.Prelude]
ls:59 [in GMu.Prelude]
ls:9 [in GMu.InfrastructureFV]
ls:98 [in GMu.Definitions]
ls:99 [in GMu.Zip]
l1:174 [in GMu.Prelude]
l2:175 [in GMu.Prelude]
L:12 [in GMu.TestVector]
l:127 [in GMu.Prelude]
L:131 [in GMu.Prelude]
l:179 [in GMu.Prelude]
L:181 [in GMu.Definitions]
L:201 [in GMu.Definitions]
L:207 [in GMu.Definitions]
L:213 [in GMu.Definitions]
L:218 [in GMu.Definitions]
L:222 [in GMu.Definitions]
L:311 [in GMu.Definitions]
L:356 [in GMu.Definitions]
L:360 [in GMu.Definitions]
L:413 [in GMu.Definitions]
L:431 [in GMu.Definitions]
L:471 [in GMu.Definitions]
L:480 [in GMu.Definitions]
L:491 [in GMu.Definitions]
l:52 [in GMu.Prelude]
l:548 [in GMu.Definitions]
L:69 [in GMu.Prelude]
L:72 [in GMu.Prelude]
L:73 [in GMu.Prelude]
l:84 [in GMu.Prelude]

M

ms:225 [in GMu.Definitions]
ms:496 [in GMu.Definitions]
ms:541 [in GMu.Definitions]
ms:573 [in GMu.Definitions]
ms:81 [in GMu.InfrastructureOpen]
m:11 [in GMu.Prelude]

N

Name:18 [in GMu.CanonicalForms]
Name:185 [in GMu.Definitions]
Name:194 [in GMu.Definitions]
Name:237 [in GMu.Definitions]
Name:319 [in GMu.Definitions]
Name:366 [in GMu.Definitions]
Name:402 [in GMu.Definitions]
Name:499 [in GMu.Definitions]
Name:5 [in GMu.CanonicalForms]
Name:91 [in GMu.Regularity]
n:10 [in GMu.InfrastructureOpen]
n:100 [in GMu.InfrastructureOpen]
n:101 [in GMu.InfrastructureOpen]
n:104 [in GMu.InfrastructureOpen]
n:107 [in GMu.InfrastructureOpen]
n:110 [in GMu.InfrastructureOpen]
n:13 [in GMu.Prelude]
N:134 [in GMu.InfrastructureOpen]
n:15 [in GMu.Prelude]
n:18 [in GMu.Prelude]
n:180 [in GMu.Prelude]
N:19 [in GMu.InfrastructureSubstPrim]
n:20 [in GMu.Prelude]
n:22 [in GMu.Prelude]
n:22 [in GMu.Definitions]
n:25 [in GMu.Prelude]
N:29 [in GMu.InfrastructureOpen]
n:3 [in GMu.InfrastructureOpen]
n:30 [in GMu.Prelude]
N:30 [in GMu.TestCommon]
n:33 [in GMu.Prelude]
n:34 [in GMu.InfrastructureOpen]
n:35 [in GMu.Prelude]
n:37 [in GMu.Prelude]
n:38 [in GMu.InfrastructureOpen]
n:40 [in GMu.Prelude]
N:44 [in GMu.CanonicalForms]
n:46 [in GMu.Definitions]
N:7 [in GMu.TestVector]
n:7 [in GMu.InfrastructureOpen]
N:76 [in GMu.InfrastructureOpen]
n:8 [in GMu.Definitions]
n:8 [in GMu.InfrastructureSubst]
n:87 [in GMu.InfrastructureOpen]
N:91 [in GMu.Equations]
n:92 [in GMu.InfrastructureOpen]
N:94 [in GMu.InfrastructureOpen]
n:95 [in GMu.InfrastructureOpen]

O

OTs:132 [in GMu.InfrastructureOpen]
O1:130 [in GMu.SubstMatch]
O1:140 [in GMu.SubstMatch]
O1:146 [in GMu.SubstMatch]
O1:146 [in GMu.InfrastructureFV]
O1:160 [in GMu.SubstMatch]
O1:173 [in GMu.SubstMatch]
O1:175 [in GMu.InfrastructureFV]
O1:186 [in GMu.SubstMatch]
O1:194 [in GMu.SubstMatch]
O1:20 [in GMu.SubstMatch]
O1:219 [in GMu.SubstMatch]
O1:238 [in GMu.SubstMatch]
O1:27 [in GMu.SubstMatch]
O1:38 [in GMu.SubstMatch]
O2:141 [in GMu.SubstMatch]
O2:147 [in GMu.SubstMatch]
O2:147 [in GMu.InfrastructureFV]
O2:174 [in GMu.SubstMatch]
O2:176 [in GMu.InfrastructureFV]
O2:187 [in GMu.SubstMatch]
O2:195 [in GMu.SubstMatch]
O2:220 [in GMu.SubstMatch]
O2:239 [in GMu.SubstMatch]
O2:29 [in GMu.SubstMatch]
O:103 [in GMu.SubstMatch]
O:108 [in GMu.SubstMatch]
O:11 [in GMu.InfrastructureSubstPrim]
O:114 [in GMu.SubstMatch]
O:119 [in GMu.SubstMatch]
O:123 [in GMu.SubstMatch]
O:14 [in GMu.InfrastructureSubstPrim]
O:143 [in GMu.InfrastructureFV]
O:148 [in GMu.InfrastructureFV]
O:17 [in GMu.InfrastructureSubstPrim]
O:178 [in GMu.InfrastructureFV]
O:181 [in GMu.SubstMatch]
O:193 [in GMu.SubstMatch]
O:21 [in GMu.InfrastructureSubstPrim]
O:22 [in GMu.InfrastructureSubstPrim]
O:231 [in GMu.SubstMatch]
O:86 [in GMu.SubstMatch]
O:9 [in GMu.InfrastructureSubstPrim]
O:93 [in GMu.SubstMatch]
O:97 [in GMu.SubstMatch]

P

Ph:134 [in GMu.Prelude]
Ps:146 [in GMu.Preservation]
Ps:173 [in GMu.InfrastructureSubst]
Ps:177 [in GMu.InfrastructureSubst]
Ps:273 [in GMu.Definitions]
Pts:135 [in GMu.Prelude]
Pt:29 [in GMu.Definitions]
P:10 [in GMu.Prelude]
P:104 [in GMu.InfrastructureFV]
P:106 [in GMu.SubstMatch]
P:111 [in GMu.SubstMatch]
P:111 [in GMu.InfrastructureSubst]
P:113 [in GMu.InfrastructureFV]
P:114 [in GMu.InfrastructureSubst]
P:117 [in GMu.InfrastructureFV]
P:12 [in GMu.InfrastructureSubst]
P:125 [in GMu.InfrastructureSubst]
P:125 [in GMu.Preservation]
P:129 [in GMu.InfrastructureSubst]
P:130 [in GMu.InfrastructureFV]
P:135 [in GMu.InfrastructureSubst]
P:135 [in GMu.Preservation]
P:14 [in GMu.Prelude]
P:148 [in GMu.Preservation]
P:154 [in GMu.Preservation]
P:161 [in GMu.InfrastructureFV]
P:168 [in GMu.InfrastructureFV]
P:170 [in GMu.InfrastructureSubst]
P:173 [in GMu.Prelude]
P:180 [in GMu.InfrastructureFV]
P:182 [in GMu.InfrastructureSubst]
P:184 [in GMu.InfrastructureFV]
P:188 [in GMu.InfrastructureFV]
p:20 [in GMu.Zip]
P:200 [in GMu.SubstMatch]
P:23 [in GMu.InfrastructureFV]
P:24 [in GMu.Prelude]
P:26 [in GMu.InfrastructureSubstPrim]
P:265 [in GMu.Definitions]
P:29 [in GMu.Prelude]
p:294 [in GMu.Definitions]
P:33 [in GMu.Zip]
P:33 [in GMu.InfrastructureSubst]
P:38 [in GMu.Regularity2]
P:39 [in GMu.Prelude]
P:39 [in GMu.InfrastructureSubst]
P:4 [in GMu.InfrastructureFV]
P:40 [in GMu.Zip]
P:44 [in GMu.Regularity2]
P:47 [in GMu.InfrastructureFV]
P:5 [in GMu.InfrastructureSubstPrim]
P:60 [in GMu.Regularity2]
P:60 [in GMu.Prelude]
P:69 [in GMu.Regularity2]
P:7 [in GMu.InfrastructureSubst]
P:82 [in GMu.InfrastructureSubst]
P:84 [in GMu.Regularity]
P:93 [in GMu.InfrastructureSubst]
P:98 [in GMu.InfrastructureSubst]

R

retTs:354 [in GMu.Definitions]
retT:363 [in GMu.Definitions]
rT:364 [in GMu.Definitions]

T

tail_proof:95 [in GMu.Definitions]
Targ:410 [in GMu.Definitions]
Tarity:350 [in GMu.Definitions]
Tarity:405 [in GMu.Definitions]
Tarity:501 [in GMu.Definitions]
Tarity:92 [in GMu.Regularity]
TA1:73 [in GMu.Equations]
TA1:79 [in GMu.Equations]
TA2:75 [in GMu.Equations]
TA2:81 [in GMu.Equations]
TB1:74 [in GMu.Equations]
TB1:80 [in GMu.Equations]
TB2:76 [in GMu.Equations]
TB2:82 [in GMu.Equations]
tc:33 [in GMu.Equations]
Tc:500 [in GMu.Definitions]
Tparams:13 [in GMu.CanonicalForms]
Tparams:184 [in GMu.Definitions]
Tparams:193 [in GMu.Definitions]
Tparams:236 [in GMu.Definitions]
Tparams:318 [in GMu.Definitions]
Tparams:4 [in GMu.CanonicalForms]
Tparams:91 [in GMu.InfrastructureSubst]
Tparam:186 [in GMu.Definitions]
Tparam:196 [in GMu.Definitions]
Tparam:94 [in GMu.InfrastructureSubst]
Tparam:95 [in GMu.InfrastructureSubst]
Tret:411 [in GMu.Definitions]
Ts':45 [in GMu.CanonicalForms]
Ts:107 [in GMu.Regularity]
ts:122 [in GMu.Definitions]
Ts:133 [in GMu.InfrastructureSubst]
Ts:155 [in GMu.InfrastructureFV]
Ts:159 [in GMu.InfrastructureSubst]
Ts:160 [in GMu.Definitions]
Ts:163 [in GMu.Definitions]
Ts:163 [in GMu.InfrastructureSubst]
Ts:168 [in GMu.Prelude]
Ts:18 [in GMu.InfrastructureSubstPrim]
Ts:192 [in GMu.Preservation]
Ts:196 [in GMu.Preservation]
Ts:210 [in GMu.SubstMatch]
Ts:22 [in GMu.TestCommon]
Ts:28 [in GMu.InfrastructureOpen]
Ts:28 [in GMu.TestCommon]
Ts:380 [in GMu.Definitions]
Ts:401 [in GMu.Definitions]
Ts:43 [in GMu.CanonicalForms]
Ts:497 [in GMu.Definitions]
Ts:52 [in GMu.Definitions]
Ts:540 [in GMu.Definitions]
Ts:61 [in GMu.Regularity2]
Ts:63 [in GMu.InfrastructureFV]
Ts:75 [in GMu.InfrastructureOpen]
Ts:79 [in GMu.InfrastructureFV]
Ts:89 [in GMu.Equations]
Ts:97 [in GMu.Equations]
Ts:98 [in GMu.InfrastructureFV]
Tts:126 [in GMu.InfrastructureSubst]
TT1:103 [in GMu.Preservation]
TT1:400 [in GMu.Definitions]
TT1:429 [in GMu.Definitions]
TT1:455 [in GMu.Definitions]
TT1:488 [in GMu.Definitions]
TT1:503 [in GMu.Definitions]
TT1:54 [in GMu.Preservation]
TT2:104 [in GMu.Preservation]
TT2:430 [in GMu.Definitions]
TT2:456 [in GMu.Definitions]
TT2:489 [in GMu.Definitions]
TT2:55 [in GMu.Preservation]
TT:103 [in GMu.InfrastructureFV]
TT:122 [in GMu.Regularity]
TT:127 [in GMu.Preservation]
TT:132 [in GMu.Regularity]
TT:136 [in GMu.Regularity]
TT:137 [in GMu.Preservation]
TT:147 [in GMu.Preservation]
TT:16 [in GMu.Preservation]
TT:163 [in GMu.Preservation]
TT:173 [in GMu.Preservation]
TT:182 [in GMu.Preservation]
TT:190 [in GMu.Preservation]
TT:23 [in GMu.Preservation]
TT:32 [in GMu.Preservation]
TT:4 [in GMu.Tests]
TT:42 [in GMu.Preservation]
TT:420 [in GMu.Definitions]
TT:437 [in GMu.Definitions]
TT:447 [in GMu.Definitions]
TT:463 [in GMu.Definitions]
TT:470 [in GMu.Definitions]
TT:477 [in GMu.Definitions]
TT:517 [in GMu.Definitions]
TT:57 [in GMu.Equations]
TT:583 [in GMu.Definitions]
TT:588 [in GMu.Definitions]
TT:63 [in GMu.Equations]
TT:8 [in GMu.Preservation]
TV:102 [in GMu.InfrastructureFV]
Typs:17 [in GMu.CanonicalForms]
Typs:9 [in GMu.CanonicalForms]
T':446 [in GMu.Definitions]
T':64 [in GMu.Equations]
T1:102 [in GMu.Equations]
T1:12 [in GMu.InfrastructureSubstPrim]
t1:13 [in GMu.Definitions]
T1:15 [in GMu.InfrastructureSubstPrim]
t1:16 [in GMu.Definitions]
T1:162 [in GMu.Preservation]
T1:172 [in GMu.Preservation]
T1:177 [in GMu.Definitions]
T1:179 [in GMu.Definitions]
t1:19 [in GMu.Definitions]
T1:20 [in GMu.InfrastructureOpen]
T1:201 [in GMu.SubstMatch]
T1:212 [in GMu.SubstMatch]
T1:216 [in GMu.SubstMatch]
T1:22 [in GMu.CanonicalForms]
T1:221 [in GMu.SubstMatch]
T1:23 [in GMu.InfrastructureOpen]
T1:247 [in GMu.SubstMatch]
T1:29 [in GMu.CanonicalForms]
T1:305 [in GMu.Definitions]
T1:309 [in GMu.Definitions]
T1:31 [in GMu.Zip]
T1:336 [in GMu.Definitions]
T1:346 [in GMu.Definitions]
T1:38 [in GMu.Zip]
T1:4 [in GMu.InfrastructureSubst]
T1:419 [in GMu.Definitions]
T1:425 [in GMu.Definitions]
T1:43 [in GMu.SubstMatch]
T1:436 [in GMu.Definitions]
T1:444 [in GMu.Definitions]
T1:451 [in GMu.Definitions]
T1:460 [in GMu.Definitions]
T1:467 [in GMu.Definitions]
T1:48 [in GMu.SubstMatch]
T1:514 [in GMu.Definitions]
T1:55 [in GMu.Equations]
t1:56 [in GMu.Definitions]
T1:61 [in GMu.SubstMatch]
T1:65 [in GMu.SubstMatch]
t1:66 [in GMu.Definitions]
t1:66 [in GMu.InfrastructureSubst]
T1:72 [in GMu.InfrastructureFV]
T1:76 [in GMu.Regularity2]
T1:8 [in GMu.SubstMatch]
T1:82 [in GMu.SubstMatch]
t1:82 [in GMu.Definitions]
T1:89 [in GMu.Regularity]
T1:9 [in GMu.InfrastructureSubst]
T2:10 [in GMu.InfrastructureSubst]
T2:103 [in GMu.Equations]
T2:13 [in GMu.InfrastructureSubstPrim]
t2:14 [in GMu.Definitions]
T2:16 [in GMu.InfrastructureSubstPrim]
T2:166 [in GMu.Preservation]
t2:17 [in GMu.Definitions]
T2:176 [in GMu.Preservation]
T2:178 [in GMu.Definitions]
T2:18 [in GMu.InfrastructureSubst]
T2:180 [in GMu.Definitions]
T2:182 [in GMu.Definitions]
T2:202 [in GMu.SubstMatch]
T2:21 [in GMu.InfrastructureOpen]
T2:213 [in GMu.SubstMatch]
T2:217 [in GMu.SubstMatch]
T2:222 [in GMu.SubstMatch]
T2:23 [in GMu.CanonicalForms]
T2:24 [in GMu.InfrastructureOpen]
T2:248 [in GMu.SubstMatch]
T2:30 [in GMu.CanonicalForms]
T2:306 [in GMu.Definitions]
T2:310 [in GMu.Definitions]
T2:314 [in GMu.Definitions]
T2:32 [in GMu.Zip]
T2:337 [in GMu.Definitions]
T2:347 [in GMu.Definitions]
T2:39 [in GMu.Zip]
T2:426 [in GMu.Definitions]
T2:44 [in GMu.SubstMatch]
T2:452 [in GMu.Definitions]
T2:461 [in GMu.Definitions]
T2:468 [in GMu.Definitions]
T2:485 [in GMu.Definitions]
T2:49 [in GMu.SubstMatch]
T2:5 [in GMu.InfrastructureSubst]
T2:515 [in GMu.Definitions]
T2:56 [in GMu.Equations]
t2:57 [in GMu.Definitions]
T2:62 [in GMu.SubstMatch]
T2:66 [in GMu.SubstMatch]
t2:67 [in GMu.Definitions]
t2:67 [in GMu.InfrastructureSubst]
T2:73 [in GMu.InfrastructureFV]
T2:77 [in GMu.Regularity2]
T2:83 [in GMu.SubstMatch]
t2:83 [in GMu.Definitions]
T2:9 [in GMu.SubstMatch]
T:1 [in GMu.Progress]
T:10 [in GMu.InfrastructureSubstPrim]
t:101 [in GMu.Definitions]
T:101 [in GMu.InfrastructureFV]
T:102 [in GMu.Regularity]
T:102 [in GMu.Preservation]
T:103 [in GMu.InfrastructureOpen]
T:106 [in GMu.InfrastructureOpen]
T:109 [in GMu.InfrastructureOpen]
T:109 [in GMu.InfrastructureFV]
T:110 [in GMu.InfrastructureFV]
T:111 [in GMu.Regularity]
T:112 [in GMu.Regularity]
T:113 [in GMu.SubstMatch]
T:114 [in GMu.InfrastructureFV]
T:116 [in GMu.Regularity]
t:117 [in GMu.Definitions]
T:118 [in GMu.SubstMatch]
T:12 [in GMu.InfrastructureFV]
T:121 [in GMu.Regularity]
T:124 [in GMu.SubstMatch]
T:125 [in GMu.Prelude]
t:125 [in GMu.Definitions]
T:125 [in GMu.InfrastructureFV]
T:126 [in GMu.Preservation]
T:128 [in GMu.InfrastructureFV]
T:13 [in GMu.TestVector]
T:130 [in GMu.InfrastructureSubst]
T:131 [in GMu.Regularity]
T:135 [in GMu.InfrastructureOpen]
T:136 [in GMu.Preservation]
T:136 [in GMu.InfrastructureOpen]
T:137 [in GMu.Prelude]
T:137 [in GMu.Definitions]
T:138 [in GMu.Regularity]
T:138 [in GMu.InfrastructureOpen]
t:139 [in GMu.Definitions]
T:139 [in GMu.InfrastructureFV]
T:141 [in GMu.Prelude]
t:141 [in GMu.Definitions]
T:142 [in GMu.SubstMatch]
T:144 [in GMu.Prelude]
T:144 [in GMu.Definitions]
T:145 [in GMu.Preservation]
T:150 [in GMu.InfrastructureFV]
T:152 [in GMu.Definitions]
T:155 [in GMu.Definitions]
T:156 [in GMu.Prelude]
T:157 [in GMu.InfrastructureFV]
T:159 [in GMu.Definitions]
T:159 [in GMu.InfrastructureFV]
T:16 [in GMu.InfrastructureSubst]
T:16 [in GMu.CanonicalForms]
T:160 [in GMu.InfrastructureSubst]
T:166 [in GMu.Definitions]
T:166 [in GMu.InfrastructureFV]
T:17 [in GMu.Regularity]
T:17 [in GMu.Equations]
T:171 [in GMu.InfrastructureSubst]
T:173 [in GMu.Definitions]
T:183 [in GMu.InfrastructureSubst]
T:183 [in GMu.Preservation]
t:191 [in GMu.Prelude]
T:194 [in GMu.Preservation]
T:2 [in GMu.Progress]
T:2 [in GMu.InfrastructureSubstPrim]
T:20 [in GMu.InfrastructureSubstPrim]
T:201 [in GMu.Preservation]
T:21 [in GMu.InfrastructureSubst]
T:210 [in GMu.Preservation]
T:211 [in GMu.Preservation]
T:212 [in GMu.Preservation]
T:213 [in GMu.Preservation]
T:214 [in GMu.Definitions]
T:214 [in GMu.Preservation]
T:215 [in GMu.Preservation]
T:216 [in GMu.Preservation]
T:217 [in GMu.Preservation]
T:218 [in GMu.SubstMatch]
T:218 [in GMu.Preservation]
T:219 [in GMu.Preservation]
T:23 [in GMu.InfrastructureSubstPrim]
T:234 [in GMu.SubstMatch]
t:24 [in GMu.Definitions]
T:24 [in GMu.TestCommon]
T:250 [in GMu.Definitions]
T:26 [in GMu.Regularity]
T:26 [in GMu.InfrastructureSubst]
T:26 [in GMu.InfrastructureOpen]
T:270 [in GMu.Definitions]
T:279 [in GMu.Definitions]
T:3 [in GMu.Regularity]
T:3 [in GMu.Equations]
T:3 [in GMu.InfrastructureSubst]
T:3 [in GMu.Tests]
T:31 [in GMu.Regularity]
T:31 [in GMu.InfrastructureOpen]
T:31 [in GMu.TestCommon]
T:322 [in GMu.Definitions]
T:323 [in GMu.Definitions]
T:333 [in GMu.Definitions]
T:35 [in GMu.CanonicalForms]
T:35 [in GMu.InfrastructureOpen]
T:36 [in GMu.InfrastructureOpen]
T:37 [in GMu.Regularity]
T:379 [in GMu.Definitions]
T:39 [in GMu.Regularity2]
T:396 [in GMu.Definitions]
t:4 [in GMu.Definitions]
T:40 [in GMu.InfrastructureOpen]
T:41 [in GMu.Prelude]
T:41 [in GMu.Preservation]
T:41 [in GMu.InfrastructureFV]
T:412 [in GMu.Definitions]
T:42 [in GMu.Prelude]
T:42 [in GMu.InfrastructureSubst]
T:43 [in GMu.Prelude]
T:445 [in GMu.Definitions]
T:45 [in GMu.Regularity2]
T:47 [in GMu.Regularity]
T:475 [in GMu.Definitions]
T:498 [in GMu.Definitions]
T:5 [in GMu.Equations]
T:51 [in GMu.Regularity2]
T:51 [in GMu.SubstMatch]
T:51 [in GMu.InfrastructureFV]
T:52 [in GMu.InfrastructureSubst]
T:520 [in GMu.Definitions]
T:525 [in GMu.Definitions]
T:53 [in GMu.Regularity]
T:53 [in GMu.Preservation]
T:534 [in GMu.Definitions]
T:54 [in GMu.Prelude]
T:54 [in GMu.InfrastructureFV]
T:557 [in GMu.Definitions]
T:57 [in GMu.InfrastructureFV]
T:58 [in GMu.Regularity2]
T:586 [in GMu.Definitions]
T:59 [in GMu.InfrastructureOpen]
T:591 [in GMu.Definitions]
T:6 [in GMu.InfrastructureSubstPrim]
T:60 [in GMu.InfrastructureFV]
T:62 [in GMu.Equations]
T:63 [in GMu.Definitions]
T:64 [in GMu.InfrastructureFV]
T:67 [in GMu.InfrastructureOpen]
T:68 [in GMu.InfrastructureFV]
T:70 [in GMu.InfrastructureOpen]
T:70 [in GMu.InfrastructureFV]
T:71 [in GMu.Regularity]
T:72 [in GMu.Definitions]
T:74 [in GMu.Regularity]
T:75 [in GMu.Definitions]
T:77 [in GMu.SubstMatch]
T:78 [in GMu.InfrastructureFV]
T:79 [in GMu.Regularity]
T:8 [in GMu.Equations]
T:8 [in GMu.CanonicalForms]
T:8 [in GMu.InfrastructureOpen]
T:82 [in GMu.InfrastructureFV]
T:85 [in GMu.Regularity]
T:85 [in GMu.Equations]
t:85 [in GMu.Definitions]
T:86 [in GMu.InfrastructureFV]
T:88 [in GMu.Prelude]
t:9 [in GMu.TestVector]
T:91 [in GMu.Prelude]
T:91 [in GMu.InfrastructureFV]
T:92 [in GMu.Equations]
T:96 [in GMu.SubstMatch]
T:96 [in GMu.InfrastructureSubst]
T:99 [in GMu.Equations]
T:99 [in GMu.InfrastructureFV]

U

Uh:31 [in GMu.InfrastructureSubst]
Uh:37 [in GMu.InfrastructureSubst]
Us:100 [in GMu.Regularity]
Us:138 [in GMu.InfrastructureSubst]
Us:153 [in GMu.InfrastructureSubst]
Us:156 [in GMu.InfrastructureFV]
Us:169 [in GMu.Prelude]
Us:193 [in GMu.Preservation]
Us:198 [in GMu.Preservation]
Us:211 [in GMu.SubstMatch]
Us:23 [in GMu.TestCommon]
Us:269 [in GMu.Definitions]
Us:29 [in GMu.TestCommon]
Us:381 [in GMu.Definitions]
Us:43 [in GMu.InfrastructureSubst]
Us:580 [in GMu.Definitions]
Us:62 [in GMu.Regularity2]
Us:90 [in GMu.Equations]
Us:98 [in GMu.Equations]
Ut:32 [in GMu.InfrastructureSubst]
Ut:38 [in GMu.InfrastructureSubst]
U0:110 [in GMu.Preservation]
U0:116 [in GMu.Preservation]
U0:137 [in GMu.SubstMatch]
U0:139 [in GMu.SubstMatch]
U0:154 [in GMu.SubstMatch]
U0:156 [in GMu.SubstMatch]
U0:167 [in GMu.SubstMatch]
U0:169 [in GMu.SubstMatch]
U0:226 [in GMu.SubstMatch]
U0:228 [in GMu.SubstMatch]
U0:61 [in GMu.Preservation]
U0:67 [in GMu.Preservation]
U0:73 [in GMu.Preservation]
U0:79 [in GMu.Preservation]
U0:87 [in GMu.Preservation]
U0:93 [in GMu.Preservation]
U1:184 [in GMu.Preservation]
U1:240 [in GMu.SubstMatch]
U1:245 [in GMu.SubstMatch]
U1:45 [in GMu.SubstMatch]
U2:185 [in GMu.Preservation]
U2:241 [in GMu.SubstMatch]
U2:246 [in GMu.SubstMatch]
U2:46 [in GMu.SubstMatch]
u:1 [in GMu.Preservation]
U:100 [in GMu.Equations]
U:100 [in GMu.Preservation]
U:103 [in GMu.Regularity]
U:108 [in GMu.Regularity]
U:11 [in GMu.Regularity]
U:113 [in GMu.InfrastructureOpen]
u:116 [in GMu.Definitions]
u:118 [in GMu.InfrastructureOpen]
u:121 [in GMu.Definitions]
U:123 [in GMu.InfrastructureSubst]
u:123 [in GMu.InfrastructureOpen]
u:124 [in GMu.Definitions]
U:126 [in GMu.SubstMatch]
U:126 [in GMu.Prelude]
u:127 [in GMu.InfrastructureOpen]
U:128 [in GMu.InfrastructureSubst]
U:129 [in GMu.SubstMatch]
u:129 [in GMu.InfrastructureOpen]
U:129 [in GMu.InfrastructureFV]
u:131 [in GMu.Definitions]
U:131 [in GMu.InfrastructureSubst]
U:135 [in GMu.SubstMatch]
U:136 [in GMu.InfrastructureSubst]
U:138 [in GMu.Definitions]
U:14 [in GMu.Preservation]
U:140 [in GMu.Definitions]
u:142 [in GMu.Definitions]
U:145 [in GMu.SubstMatch]
U:145 [in GMu.InfrastructureFV]
U:15 [in GMu.Equations]
U:15 [in GMu.InfrastructureSubst]
U:152 [in GMu.SubstMatch]
U:156 [in GMu.InfrastructureSubst]
U:157 [in GMu.InfrastructureSubst]
U:158 [in GMu.InfrastructureFV]
U:159 [in GMu.SubstMatch]
U:16 [in GMu.Regularity]
U:160 [in GMu.InfrastructureFV]
U:165 [in GMu.SubstMatch]
U:165 [in GMu.Preservation]
U:17 [in GMu.SubstMatch]
U:172 [in GMu.SubstMatch]
U:175 [in GMu.Preservation]
U:179 [in GMu.SubstMatch]
U:18 [in GMu.Equations]
U:180 [in GMu.InfrastructureSubst]
U:189 [in GMu.SubstMatch]
U:19 [in GMu.InfrastructureSubst]
U:195 [in GMu.Preservation]
U:2 [in GMu.InfrastructureSubst]
U:204 [in GMu.SubstMatch]
U:206 [in GMu.SubstMatch]
u:21 [in GMu.Preservation]
U:22 [in GMu.SubstMatch]
U:22 [in GMu.Preservation]
U:24 [in GMu.InfrastructureSubstPrim]
U:249 [in GMu.Definitions]
U:25 [in GMu.TestCommon]
U:254 [in GMu.Definitions]
u:260 [in GMu.Definitions]
U:28 [in GMu.SubstMatch]
U:280 [in GMu.Definitions]
u:30 [in GMu.Preservation]
U:31 [in GMu.Preservation]
U:32 [in GMu.TestCommon]
U:34 [in GMu.InfrastructureSubst]
U:35 [in GMu.InfrastructureSubst]
U:37 [in GMu.InfrastructureOpen]
U:382 [in GMu.Definitions]
U:39 [in GMu.SubstMatch]
U:40 [in GMu.InfrastructureSubst]
U:41 [in GMu.InfrastructureOpen]
U:46 [in GMu.InfrastructureSubst]
U:47 [in GMu.InfrastructureSubst]
U:49 [in GMu.InfrastructureSubst]
u:50 [in GMu.Preservation]
U:51 [in GMu.Preservation]
U:52 [in GMu.InfrastructureFV]
U:53 [in GMu.SubstMatch]
U:54 [in GMu.InfrastructureSubst]
U:55 [in GMu.InfrastructureFV]
U:57 [in GMu.SubstMatch]
U:57 [in GMu.InfrastructureSubst]
U:576 [in GMu.Definitions]
U:58 [in GMu.InfrastructureFV]
U:59 [in GMu.Regularity]
U:6 [in GMu.Equations]
U:6 [in GMu.Preservation]
U:60 [in GMu.InfrastructureSubst]
U:61 [in GMu.InfrastructureFV]
U:63 [in GMu.Regularity2]
u:64 [in GMu.InfrastructureSubst]
U:68 [in GMu.SubstMatch]
u:68 [in GMu.InfrastructureSubst]
U:70 [in GMu.SubstMatch]
U:70 [in GMu.Equations]
u:75 [in GMu.InfrastructureSubst]
u:79 [in GMu.InfrastructureSubst]
U:8 [in GMu.InfrastructureSubstPrim]
U:86 [in GMu.Equations]
U:88 [in GMu.SubstMatch]
U:88 [in GMu.Regularity]
u:88 [in GMu.InfrastructureSubst]
U:9 [in GMu.Equations]
u:9 [in GMu.Preservation]
U:93 [in GMu.Equations]
u:99 [in GMu.Preservation]

V

vk0:109 [in GMu.Preservation]
vk0:115 [in GMu.Preservation]
vk0:60 [in GMu.Preservation]
vk0:66 [in GMu.Preservation]
vk0:72 [in GMu.Preservation]
vk0:78 [in GMu.Preservation]
vk0:86 [in GMu.Preservation]
vk0:92 [in GMu.Preservation]
vk:10 [in GMu.Regularity]
vk:124 [in GMu.InfrastructureFV]
vk:161 [in GMu.Preservation]
vk:166 [in GMu.InfrastructureSubst]
vk:171 [in GMu.Preservation]
vk:191 [in GMu.Definitions]
vk:378 [in GMu.Definitions]
vk:395 [in GMu.Definitions]
vk:4 [in GMu.InfrastructureOpen]
vk:46 [in GMu.Regularity]
vk:48 [in GMu.InfrastructureOpen]
vk:50 [in GMu.Regularity2]
vk:52 [in GMu.Regularity]
vk:57 [in GMu.Regularity2]
vk:58 [in GMu.Regularity]
vk:70 [in GMu.Regularity]
vk:71 [in GMu.InfrastructureSubst]
vk:75 [in GMu.Regularity2]
vk:77 [in GMu.InfrastructureSubst]
vk:83 [in GMu.InfrastructureSubst]
vk:85 [in GMu.InfrastructureFV]
vk:90 [in GMu.InfrastructureOpen]
vk:90 [in GMu.InfrastructureFV]
Vs:199 [in GMu.Preservation]
v1:109 [in GMu.Prelude]
V1:132 [in GMu.SubstMatch]
V1:149 [in GMu.SubstMatch]
V1:162 [in GMu.SubstMatch]
V1:176 [in GMu.SubstMatch]
v1:211 [in GMu.Definitions]
v1:215 [in GMu.Definitions]
v1:24 [in GMu.CanonicalForms]
v1:31 [in GMu.CanonicalForms]
v1:36 [in GMu.CanonicalForms]
v1:527 [in GMu.Definitions]
v1:530 [in GMu.Definitions]
v1:532 [in GMu.Definitions]
v1:552 [in GMu.Definitions]
v1:565 [in GMu.Definitions]
v2:110 [in GMu.Prelude]
V2:133 [in GMu.SubstMatch]
V2:150 [in GMu.SubstMatch]
V2:163 [in GMu.SubstMatch]
V2:177 [in GMu.SubstMatch]
v2:25 [in GMu.CanonicalForms]
v2:522 [in GMu.Definitions]
v2:531 [in GMu.Definitions]
v2:533 [in GMu.Definitions]
V:10 [in GMu.Equations]
V:101 [in GMu.InfrastructureSubst]
v:106 [in GMu.InfrastructureSubst]
v:117 [in GMu.InfrastructureOpen]
V:122 [in GMu.InfrastructureOpen]
V:143 [in GMu.InfrastructureSubst]
V:149 [in GMu.InfrastructureSubst]
V:191 [in GMu.Preservation]
V:202 [in GMu.Definitions]
V:212 [in GMu.Definitions]
V:22 [in GMu.InfrastructureSubst]
V:230 [in GMu.Definitions]
V:28 [in GMu.InfrastructureSubst]
V:31 [in GMu.SubstMatch]
V:383 [in GMu.Definitions]
V:417 [in GMu.Definitions]
v:47 [in GMu.CanonicalForms]
v:476 [in GMu.Definitions]
V:484 [in GMu.Definitions]
v:535 [in GMu.Definitions]

X

Xs:104 [in GMu.InfrastructureSubst]
Xs:131 [in GMu.InfrastructureFV]
Xs:137 [in GMu.InfrastructureSubst]
Xs:141 [in GMu.InfrastructureSubst]
Xs:146 [in GMu.InfrastructureSubst]
Xs:151 [in GMu.InfrastructureSubst]
Xs:20 [in GMu.InfrastructureSubst]
Xs:25 [in GMu.InfrastructureSubst]
Xs:268 [in GMu.Definitions]
Xs:343 [in GMu.Definitions]
Xs:41 [in GMu.InfrastructureSubst]
Xs:579 [in GMu.Definitions]
Xs:99 [in GMu.InfrastructureSubst]
x0:108 [in GMu.Preservation]
x0:114 [in GMu.Preservation]
X0:136 [in GMu.SubstMatch]
X0:138 [in GMu.SubstMatch]
X0:153 [in GMu.SubstMatch]
X0:155 [in GMu.SubstMatch]
X0:166 [in GMu.SubstMatch]
X0:168 [in GMu.SubstMatch]
x0:59 [in GMu.Preservation]
x0:65 [in GMu.Preservation]
x0:71 [in GMu.Preservation]
x0:77 [in GMu.Preservation]
x0:85 [in GMu.Preservation]
x0:91 [in GMu.Preservation]
x:10 [in GMu.Definitions]
x:10 [in GMu.TestCommon]
X:103 [in GMu.InfrastructureSubst]
X:105 [in GMu.Preservation]
x:106 [in GMu.Prelude]
X:107 [in GMu.InfrastructureFV]
x:108 [in GMu.Prelude]
x:11 [in GMu.TestVector]
X:11 [in GMu.InfrastructureSubst]
x:11 [in GMu.InfrastructureOpen]
x:11 [in GMu.TestCommon]
X:111 [in GMu.Preservation]
X:111 [in GMu.InfrastructureFV]
X:115 [in GMu.Regularity]
X:115 [in GMu.InfrastructureFV]
x:12 [in GMu.InfrastructureOpen]
x:12 [in GMu.TestCommon]
x:120 [in GMu.InfrastructureFV]
X:123 [in GMu.Regularity]
x:123 [in GMu.Prelude]
x:123 [in GMu.InfrastructureFV]
X:124 [in GMu.Regularity]
X:125 [in GMu.SubstMatch]
X:127 [in GMu.InfrastructureFV]
X:128 [in GMu.Preservation]
X:129 [in GMu.Preservation]
X:13 [in GMu.Regularity2]
X:13 [in GMu.InfrastructureSubst]
x:13 [in GMu.TestCommon]
x:130 [in GMu.Prelude]
X:131 [in GMu.SubstMatch]
X:134 [in GMu.SubstMatch]
x:134 [in GMu.InfrastructureFV]
x:136 [in GMu.InfrastructureFV]
X:14 [in GMu.Equations]
X:144 [in GMu.InfrastructureFV]
x:145 [in GMu.Prelude]
X:145 [in GMu.InfrastructureSubst]
X:148 [in GMu.SubstMatch]
x:148 [in GMu.Prelude]
x:15 [in GMu.TestCommon]
x:150 [in GMu.Prelude]
X:150 [in GMu.InfrastructureSubst]
X:151 [in GMu.SubstMatch]
x:152 [in GMu.Prelude]
x:154 [in GMu.Prelude]
X:154 [in GMu.InfrastructureSubst]
X:155 [in GMu.InfrastructureSubst]
x:160 [in GMu.Preservation]
X:161 [in GMu.SubstMatch]
X:164 [in GMu.SubstMatch]
x:165 [in GMu.InfrastructureSubst]
x:165 [in GMu.InfrastructureFV]
X:17 [in GMu.InfrastructureSubst]
X:17 [in GMu.InfrastructureOpen]
x:17 [in GMu.TestCommon]
x:170 [in GMu.Preservation]
x:172 [in GMu.InfrastructureFV]
X:175 [in GMu.SubstMatch]
X:176 [in GMu.Definitions]
X:178 [in GMu.SubstMatch]
X:179 [in GMu.InfrastructureSubst]
X:18 [in GMu.Regularity]
x:18 [in GMu.TestCommon]
X:183 [in GMu.Definitions]
x:185 [in GMu.InfrastructureFV]
X:188 [in GMu.SubstMatch]
x:19 [in GMu.Equations]
x:192 [in GMu.Definitions]
x:2 [in GMu.Prelude]
x:2 [in GMu.InfrastructureOpen]
x:2 [in GMu.InfrastructureFV]
X:20 [in GMu.Regularity]
x:202 [in GMu.Preservation]
X:203 [in GMu.SubstMatch]
x:203 [in GMu.Preservation]
x:204 [in GMu.Definitions]
x:204 [in GMu.Preservation]
X:205 [in GMu.SubstMatch]
x:205 [in GMu.Preservation]
x:206 [in GMu.Preservation]
x:207 [in GMu.Preservation]
X:209 [in GMu.Definitions]
X:21 [in GMu.SubstMatch]
x:21 [in GMu.Equations]
X:210 [in GMu.Definitions]
x:216 [in GMu.Definitions]
x:217 [in GMu.Definitions]
x:220 [in GMu.Preservation]
x:221 [in GMu.Definitions]
x:221 [in GMu.Preservation]
X:225 [in GMu.SubstMatch]
X:227 [in GMu.SubstMatch]
x:228 [in GMu.Definitions]
x:23 [in GMu.Equations]
x:233 [in GMu.Definitions]
X:24 [in GMu.InfrastructureSubst]
X:25 [in GMu.SubstMatch]
x:25 [in GMu.Equations]
X:286 [in GMu.Definitions]
X:29 [in GMu.InfrastructureSubst]
x:3 [in GMu.Prelude]
X:302 [in GMu.Definitions]
X:315 [in GMu.Definitions]
X:32 [in GMu.InfrastructureOpen]
X:36 [in GMu.SubstMatch]
x:37 [in GMu.InfrastructureFV]
x:377 [in GMu.Definitions]
x:394 [in GMu.Definitions]
x:4 [in GMu.Prelude]
x:421 [in GMu.Definitions]
X:438 [in GMu.Definitions]
X:439 [in GMu.Definitions]
X:44 [in GMu.InfrastructureSubst]
x:45 [in GMu.Regularity]
X:45 [in GMu.InfrastructureSubst]
x:46 [in GMu.InfrastructureFV]
x:47 [in GMu.Prelude]
x:47 [in GMu.InfrastructureOpen]
x:478 [in GMu.Definitions]
x:479 [in GMu.Definitions]
X:48 [in GMu.InfrastructureSubst]
x:49 [in GMu.Regularity2]
x:49 [in GMu.Definitions]
x:49 [in GMu.Preservation]
x:490 [in GMu.Definitions]
x:5 [in GMu.Prelude]
x:509 [in GMu.Definitions]
x:51 [in GMu.Regularity]
X:53 [in GMu.InfrastructureSubst]
X:55 [in GMu.InfrastructureSubst]
x:56 [in GMu.Regularity2]
X:56 [in GMu.SubstMatch]
X:56 [in GMu.Preservation]
x:57 [in GMu.Regularity]
X:59 [in GMu.InfrastructureSubst]
x:6 [in GMu.Prelude]
X:6 [in GMu.InfrastructureSubst]
x:6 [in GMu.InfrastructureOpen]
x:62 [in GMu.InfrastructureSubst]
X:62 [in GMu.Preservation]
X:65 [in GMu.Regularity]
X:65 [in GMu.InfrastructureFV]
X:67 [in GMu.SubstMatch]
X:67 [in GMu.InfrastructureFV]
x:68 [in GMu.Prelude]
X:68 [in GMu.Preservation]
x:69 [in GMu.Regularity]
x:7 [in GMu.Prelude]
X:7 [in GMu.InfrastructureSubstPrim]
x:70 [in GMu.InfrastructureSubst]
x:71 [in GMu.Prelude]
x:71 [in GMu.InfrastructureFV]
x:72 [in GMu.InfrastructureSubst]
x:74 [in GMu.Regularity2]
X:74 [in GMu.Preservation]
X:76 [in GMu.SubstMatch]
x:77 [in GMu.InfrastructureFV]
x:78 [in GMu.InfrastructureSubst]
x:8 [in GMu.Prelude]
x:8 [in GMu.InfrastructureFV]
x:81 [in GMu.InfrastructureFV]
X:82 [in GMu.Preservation]
x:84 [in GMu.InfrastructureSubst]
x:84 [in GMu.InfrastructureFV]
x:85 [in GMu.Prelude]
X:85 [in GMu.InfrastructureOpen]
x:86 [in GMu.Prelude]
X:87 [in GMu.SubstMatch]
X:88 [in GMu.Preservation]
X:88 [in GMu.InfrastructureFV]
x:89 [in GMu.Prelude]
x:89 [in GMu.InfrastructureOpen]
x:89 [in GMu.InfrastructureFV]
x:9 [in GMu.Regularity]
x:9 [in GMu.Prelude]
X:9 [in GMu.InfrastructureOpen]
X:90 [in GMu.InfrastructureSubst]
X:91 [in GMu.SubstMatch]
x:92 [in GMu.Prelude]
X:94 [in GMu.InfrastructureFV]
X:95 [in GMu.SubstMatch]
x:97 [in GMu.Prelude]
X:97 [in GMu.InfrastructureFV]
X:98 [in GMu.SubstMatch]
x:98 [in GMu.Preservation]
x:98 [in GMu.InfrastructureOpen]
x:99 [in GMu.InfrastructureOpen]

Y

Y:102 [in GMu.InfrastructureSubst]
y:107 [in GMu.InfrastructureSubst]
y:124 [in GMu.Prelude]
Y:13 [in GMu.SubstMatch]
Y:14 [in GMu.InfrastructureSubst]
Y:144 [in GMu.InfrastructureSubst]
Y:148 [in GMu.InfrastructureSubst]
Y:15 [in GMu.Preservation]
y:16 [in GMu.TestCommon]
Y:23 [in GMu.InfrastructureSubst]
Y:27 [in GMu.InfrastructureSubst]
Y:30 [in GMu.SubstMatch]
Y:50 [in GMu.SubstMatch]
Y:56 [in GMu.InfrastructureSubst]
Y:66 [in GMu.InfrastructureFV]
Y:68 [in GMu.Equations]
y:73 [in GMu.InfrastructureSubst]
Y:81 [in GMu.SubstMatch]
y:87 [in GMu.Prelude]
y:90 [in GMu.Prelude]

Z

z':62 [in GMu.Prelude]
Z:1 [in GMu.InfrastructureSubst]
Z:106 [in GMu.InfrastructureFV]
Z:110 [in GMu.InfrastructureSubst]
Z:112 [in GMu.InfrastructureFV]
Z:113 [in GMu.InfrastructureSubst]
Z:116 [in GMu.InfrastructureSubst]
Z:116 [in GMu.InfrastructureFV]
z:117 [in GMu.Prelude]
Z:120 [in GMu.InfrastructureSubst]
Z:121 [in GMu.InfrastructureFV]
Z:123 [in GMu.Preservation]
Z:124 [in GMu.InfrastructureSubst]
Z:127 [in GMu.InfrastructureSubst]
Z:13 [in GMu.InfrastructureFV]
Z:132 [in GMu.InfrastructureSubst]
Z:133 [in GMu.Preservation]
Z:134 [in GMu.InfrastructureSubst]
Z:164 [in GMu.Definitions]
Z:169 [in GMu.InfrastructureSubst]
Z:179 [in GMu.InfrastructureFV]
Z:183 [in GMu.InfrastructureFV]
Z:185 [in GMu.InfrastructureSubst]
Z:187 [in GMu.InfrastructureFV]
Z:188 [in GMu.InfrastructureSubst]
Z:199 [in GMu.SubstMatch]
Z:21 [in GMu.InfrastructureFV]
Z:248 [in GMu.Definitions]
Z:253 [in GMu.Definitions]
z:258 [in GMu.Definitions]
Z:264 [in GMu.Definitions]
Z:28 [in GMu.InfrastructureFV]
Z:36 [in GMu.InfrastructureFV]
Z:37 [in GMu.Regularity2]
Z:43 [in GMu.Regularity2]
z:45 [in GMu.InfrastructureFV]
Z:59 [in GMu.Regularity2]
z:61 [in GMu.Prelude]
Z:68 [in GMu.Regularity2]
Z:81 [in GMu.InfrastructureSubst]
Z:83 [in GMu.Regularity]
z:86 [in GMu.InfrastructureSubst]
Z:92 [in GMu.InfrastructureSubst]
Z:97 [in GMu.InfrastructureSubst]

other

Δ1:120 [in GMu.Preservation]
Δ1:128 [in GMu.SubstMatch]
Δ1:144 [in GMu.SubstMatch]
Δ1:158 [in GMu.SubstMatch]
Δ1:171 [in GMu.SubstMatch]
Δ1:178 [in GMu.Preservation]
Δ1:184 [in GMu.SubstMatch]
Δ1:191 [in GMu.SubstMatch]
Δ1:197 [in GMu.SubstMatch]
Δ1:236 [in GMu.SubstMatch]
Δ1:243 [in GMu.SubstMatch]
Δ2:121 [in GMu.Preservation]
Δ2:141 [in GMu.Preservation]
Δ2:179 [in GMu.Preservation]
Δ2:185 [in GMu.SubstMatch]
Δ2:192 [in GMu.SubstMatch]
Δ2:198 [in GMu.SubstMatch]
Δ2:237 [in GMu.SubstMatch]
Δ2:244 [in GMu.SubstMatch]
Δ:101 [in GMu.Regularity]
Δ:104 [in GMu.SubstMatch]
Δ:104 [in GMu.Regularity]
Δ:109 [in GMu.SubstMatch]
Δ:11 [in GMu.CanonicalForms]
Δ:114 [in GMu.Regularity]
Δ:115 [in GMu.SubstMatch]
Δ:118 [in GMu.Regularity]
Δ:12 [in GMu.Equations]
Δ:120 [in GMu.SubstMatch]
Δ:122 [in GMu.SubstMatch]
Δ:126 [in GMu.InfrastructureFV]
Δ:128 [in GMu.Regularity]
Δ:131 [in GMu.Preservation]
Δ:134 [in GMu.Regularity]
Δ:138 [in GMu.InfrastructureFV]
Δ:140 [in GMu.Preservation]
Δ:157 [in GMu.Preservation]
Δ:16 [in GMu.Equations]
Δ:168 [in GMu.Preservation]
Δ:18 [in GMu.Preservation]
Δ:182 [in GMu.SubstMatch]
Δ:182 [in GMu.InfrastructureFV]
Δ:186 [in GMu.InfrastructureFV]
Δ:187 [in GMu.Preservation]
Δ:2 [in GMu.Equations]
Δ:2 [in GMu.CanonicalForms]
Δ:20 [in GMu.CanonicalForms]
Δ:208 [in GMu.SubstMatch]
Δ:215 [in GMu.SubstMatch]
Δ:27 [in GMu.CanonicalForms]
Δ:27 [in GMu.Preservation]
Δ:27 [in GMu.TestCommon]
Δ:285 [in GMu.Definitions]
Δ:287 [in GMu.Definitions]
Δ:290 [in GMu.Definitions]
Δ:299 [in GMu.Definitions]
Δ:301 [in GMu.Definitions]
Δ:304 [in GMu.Definitions]
Δ:308 [in GMu.Definitions]
Δ:313 [in GMu.Definitions]
Δ:317 [in GMu.Definitions]
Δ:32 [in GMu.Equations]
Δ:33 [in GMu.CanonicalForms]
Δ:331 [in GMu.Definitions]
Δ:335 [in GMu.Definitions]
Δ:339 [in GMu.Definitions]
Δ:34 [in GMu.TestCommon]
Δ:345 [in GMu.Definitions]
Δ:357 [in GMu.Definitions]
Δ:36 [in GMu.Regularity]
Δ:36 [in GMu.Preservation]
Δ:361 [in GMu.Definitions]
Δ:37 [in GMu.Equations]
Δ:373 [in GMu.Definitions]
Δ:375 [in GMu.Definitions]
Δ:38 [in GMu.CanonicalForms]
Δ:389 [in GMu.Definitions]
Δ:393 [in GMu.Definitions]
Δ:399 [in GMu.Definitions]
Δ:4 [in GMu.Equations]
Δ:40 [in GMu.Regularity]
Δ:41 [in GMu.CanonicalForms]
Δ:415 [in GMu.Definitions]
Δ:423 [in GMu.Definitions]
Δ:43 [in GMu.Regularity]
Δ:433 [in GMu.Definitions]
Δ:441 [in GMu.Definitions]
Δ:449 [in GMu.Definitions]
Δ:45 [in GMu.Equations]
Δ:458 [in GMu.Definitions]
Δ:46 [in GMu.Preservation]
Δ:465 [in GMu.Definitions]
Δ:47 [in GMu.Regularity2]
Δ:473 [in GMu.Definitions]
Δ:482 [in GMu.Definitions]
Δ:49 [in GMu.Regularity]
Δ:493 [in GMu.Definitions]
Δ:5 [in GMu.Regularity]
Δ:512 [in GMu.Definitions]
Δ:52 [in GMu.Equations]
Δ:53 [in GMu.Regularity2]
Δ:55 [in GMu.Regularity]
Δ:59 [in GMu.Equations]
Δ:66 [in GMu.Equations]
Δ:67 [in GMu.Regularity]
Δ:7 [in GMu.Equations]
Δ:71 [in GMu.Regularity2]
Δ:72 [in GMu.Equations]
Δ:73 [in GMu.Regularity]
Δ:78 [in GMu.Equations]
Δ:8 [in GMu.Regularity]
Δ:84 [in GMu.Equations]
Δ:87 [in GMu.Regularity]
Δ:88 [in GMu.Equations]
Δ:94 [in GMu.SubstMatch]
Δ:95 [in GMu.Preservation]
Θ1:15 [in GMu.SubstMatch]
Θ1:54 [in GMu.SubstMatch]
Θ1:63 [in GMu.SubstMatch]
Θ1:72 [in GMu.SubstMatch]
Θ2:16 [in GMu.SubstMatch]
Θ2:55 [in GMu.SubstMatch]
Θ2:64 [in GMu.SubstMatch]
Θ2:73 [in GMu.SubstMatch]
Θ:1 [in GMu.InfrastructureSubstPrim]
Θ:13 [in GMu.Equations]
Θ:14 [in GMu.SubstMatch]
Θ:276 [in GMu.Definitions]
Θ:3 [in GMu.SubstMatch]
Θ:3 [in GMu.InfrastructureSubstPrim]
Θ:31 [in GMu.Equations]
Θ:324 [in GMu.Definitions]
Θ:330 [in GMu.Definitions]
Θ:334 [in GMu.Definitions]
Θ:342 [in GMu.Definitions]
Θ:38 [in GMu.Equations]
Θ:41 [in GMu.Equations]
Θ:47 [in GMu.SubstMatch]
Θ:5 [in GMu.SubstMatch]
Θ:67 [in GMu.Equations]
Σ:1 [in GMu.Regularity2]
Σ:1 [in GMu.SubstMatch]
Σ:1 [in GMu.Regularity]
Σ:1 [in GMu.CanonicalForms]
Σ:1 [in GMu.Tests]
Σ:10 [in GMu.SubstMatch]
Σ:10 [in GMu.CanonicalForms]
Σ:10 [in GMu.Preservation]
Σ:101 [in GMu.Equations]
Σ:102 [in GMu.SubstMatch]
Σ:105 [in GMu.Regularity]
Σ:107 [in GMu.SubstMatch]
Σ:11 [in GMu.Equations]
Σ:112 [in GMu.SubstMatch]
Σ:113 [in GMu.Regularity]
Σ:117 [in GMu.SubstMatch]
Σ:117 [in GMu.Regularity]
Σ:119 [in GMu.Preservation]
Σ:121 [in GMu.SubstMatch]
Σ:127 [in GMu.SubstMatch]
Σ:127 [in GMu.Regularity]
Σ:13 [in GMu.Regularity]
Σ:130 [in GMu.Preservation]
Σ:133 [in GMu.Regularity]
Σ:137 [in GMu.InfrastructureFV]
Σ:139 [in GMu.Preservation]
Σ:14 [in GMu.Regularity2]
Σ:143 [in GMu.SubstMatch]
Σ:156 [in GMu.Preservation]
Σ:157 [in GMu.SubstMatch]
Σ:167 [in GMu.Preservation]
Σ:17 [in GMu.Preservation]
Σ:170 [in GMu.SubstMatch]
Σ:177 [in GMu.Preservation]
Σ:18 [in GMu.SubstMatch]
Σ:180 [in GMu.SubstMatch]
Σ:183 [in GMu.SubstMatch]
Σ:186 [in GMu.Preservation]
Σ:19 [in GMu.Regularity2]
Σ:19 [in GMu.CanonicalForms]
Σ:190 [in GMu.SubstMatch]
Σ:196 [in GMu.SubstMatch]
Σ:2 [in GMu.Preservation]
Σ:207 [in GMu.SubstMatch]
Σ:214 [in GMu.SubstMatch]
Σ:22 [in GMu.Regularity]
Σ:229 [in GMu.SubstMatch]
Σ:23 [in GMu.SubstMatch]
Σ:235 [in GMu.SubstMatch]
Σ:242 [in GMu.SubstMatch]
Σ:26 [in GMu.Regularity2]
Σ:26 [in GMu.CanonicalForms]
Σ:26 [in GMu.Preservation]
Σ:26 [in GMu.TestCommon]
Σ:27 [in GMu.Regularity]
Σ:29 [in GMu.Equations]
Σ:298 [in GMu.Definitions]
Σ:300 [in GMu.Definitions]
Σ:303 [in GMu.Definitions]
Σ:307 [in GMu.Definitions]
Σ:312 [in GMu.Definitions]
Σ:316 [in GMu.Definitions]
Σ:32 [in GMu.CanonicalForms]
Σ:327 [in GMu.Definitions]
Σ:33 [in GMu.TestCommon]
Σ:338 [in GMu.Definitions]
Σ:34 [in GMu.Regularity2]
Σ:34 [in GMu.SubstMatch]
Σ:34 [in GMu.Regularity]
Σ:344 [in GMu.Definitions]
Σ:35 [in GMu.Preservation]
Σ:353 [in GMu.Definitions]
Σ:36 [in GMu.Equations]
Σ:365 [in GMu.Definitions]
Σ:37 [in GMu.CanonicalForms]
Σ:372 [in GMu.Definitions]
Σ:374 [in GMu.Definitions]
Σ:388 [in GMu.Definitions]
Σ:39 [in GMu.Regularity]
Σ:391 [in GMu.Definitions]
Σ:397 [in GMu.Definitions]
Σ:4 [in GMu.SubstMatch]
Σ:4 [in GMu.Regularity]
Σ:40 [in GMu.Regularity2]
Σ:40 [in GMu.SubstMatch]
Σ:40 [in GMu.CanonicalForms]
Σ:414 [in GMu.Definitions]
Σ:42 [in GMu.Regularity]
Σ:422 [in GMu.Definitions]
Σ:432 [in GMu.Definitions]
Σ:44 [in GMu.Equations]
Σ:440 [in GMu.Definitions]
Σ:448 [in GMu.Definitions]
Σ:45 [in GMu.Preservation]
Σ:457 [in GMu.Definitions]
Σ:46 [in GMu.Regularity2]
Σ:464 [in GMu.Definitions]
Σ:472 [in GMu.Definitions]
Σ:48 [in GMu.Regularity]
Σ:481 [in GMu.Definitions]
Σ:492 [in GMu.Definitions]
Σ:5 [in GMu.Regularity2]
Σ:50 [in GMu.Equations]
Σ:51 [in GMu.Equations]
Σ:511 [in GMu.Definitions]
Σ:52 [in GMu.Regularity2]
Σ:54 [in GMu.Regularity]
Σ:58 [in GMu.SubstMatch]
Σ:58 [in GMu.Equations]
Σ:584 [in GMu.Definitions]
Σ:589 [in GMu.Definitions]
Σ:61 [in GMu.Regularity]
Σ:64 [in GMu.Regularity2]
Σ:65 [in GMu.Equations]
Σ:66 [in GMu.Regularity]
Σ:7 [in GMu.Regularity]
Σ:70 [in GMu.Regularity2]
Σ:71 [in GMu.SubstMatch]
Σ:71 [in GMu.Equations]
Σ:72 [in GMu.Regularity]
Σ:75 [in GMu.Regularity]
Σ:77 [in GMu.Equations]
Σ:78 [in GMu.Regularity2]
Σ:78 [in GMu.SubstMatch]
Σ:80 [in GMu.Regularity]
Σ:83 [in GMu.Equations]
Σ:84 [in GMu.SubstMatch]
Σ:86 [in GMu.Regularity]
Σ:87 [in GMu.Equations]
Σ:9 [in GMu.Regularity2]
Σ:90 [in GMu.Regularity]
Σ:92 [in GMu.SubstMatch]
Σ:94 [in GMu.Preservation]
Σ:98 [in GMu.Regularity]
ϵ:142 [in GMu.InfrastructureFV]
ϵ:171 [in GMu.Prelude]
ϵ:25 [in GMu.Regularity2]
ϵ:25 [in GMu.Regularity]
ϵ:25 [in GMu.Preservation]
ϵ:33 [in GMu.Regularity]

---

Variable Index

M

ManyTest.T [in GMu.DefinitionsTests]

S

SimpleEquationProperties.Σ [in GMu.Equations]

T

trm_ind'.trm_let_case [in GMu.Definitions]
trm_ind'.trm_match_case [in GMu.Definitions]
trm_ind'.trm_fix_case [in GMu.Definitions]
trm_ind'.trm_tapp_case [in GMu.Definitions]
trm_ind'.trm_tabs_case [in GMu.Definitions]
trm_ind'.trm_app_case [in GMu.Definitions]
trm_ind'.trm_abs_case [in GMu.Definitions]
trm_ind'.trm_snd_case [in GMu.Definitions]
trm_ind'.trm_fst_case [in GMu.Definitions]
trm_ind'.trm_tuple_case [in GMu.Definitions]
trm_ind'.trm_unit_case [in GMu.Definitions]
trm_ind'.trm_constructor_case [in GMu.Definitions]
trm_ind'.trm_fvar_case [in GMu.Definitions]
trm_ind'.trm_bvar_case [in GMu.Definitions]
trm_ind'.P [in GMu.Definitions]
typ_ind'.typ_gadt_case [in GMu.Definitions]
typ_ind'.typ_all_case [in GMu.Definitions]
typ_ind'.typ_arrow_case [in GMu.Definitions]
typ_ind'.typ_tuple_case [in GMu.Definitions]
typ_ind'.typ_unit_case [in GMu.Definitions]
typ_ind'.typ_fvar_case [in GMu.Definitions]
typ_ind'.typ_bvar_case [in GMu.Definitions]
typ_ind'.P [in GMu.Definitions]

Z

Zip.A [in GMu.Zip]
Zip.B [in GMu.Zip]
Zip.R [in GMu.Zip]

---

Library Index

C

CanonicalForms

D

Definitions
DefinitionsTests

E

Equations

I

Infrastructure
InfrastructureFV
InfrastructureOpen
InfrastructureSubst
InfrastructureSubstPrim

N

Notations

P

Prelude
Preservation
Progress

R

Regularity
Regularity2

S

SubstMatch

T

TestCommon
TestEquality
Tests
Tests2
TestVector

Z

Zip

---

Lemma Index

A

all_distinct [in GMu.Tests2]

B

binds_ext [in GMu.Prelude]

C

CanonicalConstructorType [in GMu.CanonicalForms]
CanonicalConstructorTypeGen [in GMu.CanonicalForms]
CanonicalFormAbs [in GMu.CanonicalForms]
CanonicalFormGadt [in GMu.CanonicalForms]
CanonicalFormTAbs [in GMu.CanonicalForms]
CanonicalFormTuple [in GMu.CanonicalForms]
CanonicalFormUnit [in GMu.CanonicalForms]
closed_id [in GMu.InfrastructureOpen]
coerce_types [in GMu.TestEquality]
construct_types [in GMu.TestEquality]
const_test_evals [in GMu.Tests2]
const_test_types [in GMu.Tests2]
const_types [in GMu.Tests2]
cons_type [in GMu.TestVector]
contradictory_env_test [in GMu.Equations]
contradictory_env_test_0 [in GMu.Equations]

D

destruct_types [in GMu.TestEquality]
distinct_split1 [in GMu.InfrastructureFV]
divergent_diverges [in GMu.Tests]
divergent_type [in GMu.Tests]
domDelta_subst_td [in GMu.InfrastructureFV]
domDelta_app [in GMu.InfrastructureFV]
domDelta_in [in GMu.InfrastructureFV]

E

empty_eq_is_equivalent [in GMu.Equations]
empty_is_not_contradictory [in GMu.Equations]
empty_inter_implies_notin [in GMu.Prelude]
entails_through_subst [in GMu.SubstMatch]
env_map_compose [in GMu.Prelude]
equations_weaken_match [in GMu.SubstMatch]
equations_from_lists_map [in GMu.Equations]
equations_from_lists_are_equations [in GMu.Prelude]
equations_have_no_dom [in GMu.InfrastructureFV]
equation_strengthen [in GMu.SubstMatch]
equation_weaken_var [in GMu.SubstMatch]
equation_weaken_eq [in GMu.SubstMatch]
eq_dec_var [in GMu.Prelude]
eq_typ_tuple [in GMu.TestCommon]
eq_typ_gadt [in GMu.TestCommon]
exist_alphas [in GMu.Prelude]
ext_in_map [in GMu.Prelude]

F

fold_left_subset [in GMu.InfrastructureFV]
fold_left_subset_base [in GMu.InfrastructureFV]
fold_empty [in GMu.InfrastructureFV]
forall2_from_snd_zip [in GMu.Zip]
forall2_from_snd [in GMu.Zip]
Forall2_eq_len [in GMu.Prelude]
Forall2_eq [in GMu.TestCommon]
from_list_spec2 [in GMu.Prelude]
from_list_spec [in GMu.Prelude]
fst_from_zip [in GMu.Zip]
fv_typs_migration [in GMu.Definitions]
fv_delta_equations [in GMu.InfrastructureFV]
fv_delta_alphas [in GMu.InfrastructureFV]
fv_delta_app [in GMu.InfrastructureFV]
fv_env_subst [in GMu.InfrastructureFV]
fv_subst_tt [in GMu.InfrastructureFV]
fv_env_extend [in GMu.InfrastructureFV]
fv_open_te_many [in GMu.InfrastructureFV]
fv_open_te [in GMu.InfrastructureFV]
fv_open_tt [in GMu.InfrastructureFV]
fv_smaller_many [in GMu.InfrastructureFV]
fv_typs_notin [in GMu.InfrastructureFV]
fv_smaller [in GMu.InfrastructureFV]
fv_open [in GMu.InfrastructureFV]
fv_fold_in [in GMu.InfrastructureFV]
fv_fold_in_clause [in GMu.InfrastructureFV]
fv_fold_in_general [in GMu.InfrastructureFV]
fv_fold_base_clause [in GMu.InfrastructureFV]
fv_fold_base [in GMu.InfrastructureFV]
fv_fold_general [in GMu.InfrastructureFV]
F2_from_zip [in GMu.Zip]
F2_iff_In_zip [in GMu.Zip]

G

gadt_constructor_ok [in GMu.Regularity]

H

head_types [in GMu.TestVector]
helper_equations_commute [in GMu.Preservation]

I

id_app_evals [in GMu.Tests]
id_app_types [in GMu.Tests]
inversion_eq_typ_gadt [in GMu.Equations]
inversion_eq_typ_all [in GMu.Equations]
inversion_eq_tuple [in GMu.Equations]
inversion_eq_arrow [in GMu.Equations]
inversion_typing_eq [in GMu.Equations]
Inzip_from_nth_error [in GMu.Zip]
Inzip_to_nth_error [in GMu.Zip]
inzip_map_clause_trm [in GMu.Prelude]
in_from_list [in GMu.Prelude]
in_fold_exists [in GMu.InfrastructureFV]
in_domΔ_eq [in GMu.InfrastructureFV]
is_var_defined_split [in GMu.SubstMatch]
is_var_defined_dom [in GMu.SubstMatch]
is_var_defined_split [in GMu.TestCommon]

J

JMeq_from_eq [in GMu.Prelude]

L

length_equality [in GMu.Prelude]
let_id_app_evals [in GMu.Tests]
let_id_app_types [in GMu.Tests]
LibList_mem [in GMu.Prelude]
LibList_map [in GMu.Prelude]
lists_map_eq [in GMu.Prelude]
list_fold_map [in GMu.Prelude]
loop_type [in GMu.Tests]

M

map_types [in GMu.TestVector]
map_map [in GMu.Prelude]
map_id [in GMu.Prelude]

N

neq_from_notin [in GMu.TestCommon]
nil_type [in GMu.TestVector]
notin_eqv [in GMu.TestVector]
notin_fv_wf [in GMu.Regularity]
notin_from_list [in GMu.Equations]
notin_inverse [in GMu.Prelude]
notin_domDelta_subst_td [in GMu.InfrastructureFV]
notin_env_binds [in GMu.InfrastructureFV]
notin_dom_tc_vars [in GMu.InfrastructureFV]
notin_domΔ_eq [in GMu.InfrastructureFV]
notin_env_inv [in GMu.InfrastructureFV]
notin_fv_tt_open [in GMu.InfrastructureFV]
notin_fold [in GMu.InfrastructureFV]
nth_error_map [in GMu.Zip]
nth_error_zip_merge [in GMu.Zip]
nth_error_zip_split [in GMu.Zip]
nth_error_implies_zip_swap [in GMu.Zip]
nth_error_implies_zip [in GMu.Zip]
nth_error_map [in GMu.Prelude]

O

oknat [in GMu.Tests2]
oksigma [in GMu.TestVector]
oksigma [in GMu.TestEquality]
okt_strengthen_delta_eq [in GMu.Regularity2]
okt_replace_typ [in GMu.Regularity2]
okt_through_subst_tdtb [in GMu.Regularity2]
okt_is_wft_2 [in GMu.Regularity2]
okt_push_fresh [in GMu.Regularity2]
okt_weakening_delta_many [in GMu.Regularity2]
okt_weakening_delta_many_eq [in GMu.Regularity2]
okt_weakening_delta_eq [in GMu.Regularity2]
okt_weakening_delta [in GMu.Regularity2]
okt_strengthen_simple [in GMu.Regularity2]
okt_is_type [in GMu.Regularity]
okt_strengthen_delta_var [in GMu.Regularity]
okt_strengthen [in GMu.Regularity]
okt_is_wft [in GMu.Regularity]
okt_push_var_inv [in GMu.Regularity]
okt_implies_okgadt [in GMu.Regularity]
okt_is_ok [in GMu.Regularity]
one_type [in GMu.Tests2]
only_vars_is_tc_vars [in GMu.Equations]
opening_adds_one [in GMu.InfrastructureOpen]
open_te_many_test [in GMu.DefinitionsTests]
open_tt_many_test [in GMu.DefinitionsTests]
open_typlist_test [in GMu.DefinitionsTests]
open_ee_test [in GMu.DefinitionsTests]
open_te_test [in GMu.DefinitionsTests]
open_tt_test [in GMu.DefinitionsTests]
open_tt_many_closed [in GMu.InfrastructureOpen]
open_ee_rec_term [in GMu.InfrastructureOpen]
open_ee_rec_type_many [in GMu.InfrastructureOpen]
open_ee_rec_type_core [in GMu.InfrastructureOpen]
open_ee_rec_term_core [in GMu.InfrastructureOpen]
open_te_rec_term [in GMu.InfrastructureOpen]
open_tt_rec_type [in GMu.InfrastructureOpen]
open_tt_var_preserves_size [in GMu.InfrastructureOpen]
open_te_var_preserves_size [in GMu.InfrastructureOpen]
open_ee_var_preserves_size [in GMu.InfrastructureOpen]

P

plus_evals4 [in GMu.Tests2]
plus_evals [in GMu.Tests2]
plus_types [in GMu.Tests2]
preservation_thm [in GMu.Preservation]
preservation_evals [in GMu.Tests]
progress_thm [in GMu.Progress]

R

remove_true_equations [in GMu.Preservation]
remove_true_equation [in GMu.Preservation]
rewrite_open_tt_many_gadt [in GMu.InfrastructureOpen]

S

snd_from_zip [in GMu.Zip]
sources_distinct [in GMu.SubstMatch]
sources_list_fst [in GMu.InfrastructureFV]
spawn_unit_subst [in GMu.Equations]
split_notin_subset_union [in GMu.Prelude]
strong_induction_on_typ_size [in GMu.Prelude]
strong_induction_on_type_size_helper [in GMu.Prelude]
strong_induction_on_term_size [in GMu.Prelude]
strong_induction_on_term_size_helper [in GMu.Prelude]
strong_induction [in GMu.Prelude]
sublist_head_prop [in GMu.InfrastructureSubst]
sublist_tail_prop [in GMu.InfrastructureSubst]
subset_transitive [in GMu.Prelude]
subset_fold [in GMu.InfrastructureFV]
substitution_sources_from_in [in GMu.InfrastructureFV]
subst_td_eqs [in GMu.Regularity2]
subst_strengthen_true_eq [in GMu.SubstMatch]
subst_match_inv_missing_var [in GMu.SubstMatch]
subst_eq_weaken2 [in GMu.SubstMatch]
subst_match_split [in GMu.SubstMatch]
subst_remove_used_var [in GMu.SubstMatch]
subst_eq_reorder2 [in GMu.SubstMatch]
subst_eq_reorder2_2 [in GMu.SubstMatch]
subst_eq_reorder1 [in GMu.SubstMatch]
subst_tt_split [in GMu.SubstMatch]
subst_eq_reorder1_2 [in GMu.SubstMatch]
subst_idempotent_simple [in GMu.SubstMatch]
subst_has_closed [in GMu.SubstMatch]
subst_has_wft [in GMu.SubstMatch]
subst_tt_prime_reduce_typ_fvar_undefined [in GMu.SubstMatch]
subst_tt_prime_reduce_typ_fvar_defined [in GMu.SubstMatch]
subst_match_remove_right_var3 [in GMu.SubstMatch]
subst_match_remove_unused_var [in GMu.SubstMatch]
subst_eq_weaken [in GMu.SubstMatch]
subst_eq_strengthen_gen [in GMu.SubstMatch]
subst_eq_strengthen [in GMu.SubstMatch]
subst_match_remove_right_var2 [in GMu.SubstMatch]
subst_match_remove_right_var [in GMu.SubstMatch]
subst_match_notin_srcs [in GMu.SubstMatch]
subst_match_decompose_var [in GMu.SubstMatch]
subst_match_remove_eq [in GMu.SubstMatch]
subst_sources_from_match [in GMu.SubstMatch]
subst_has_no_fv2 [in GMu.Equations]
subst_ttΘ_into_tuple [in GMu.Equations]
subst_ttΘ_into_abs [in GMu.Equations]
subst_has_no_fv [in GMu.Equations]
subst_tb_many_split [in GMu.Prelude]
subst_ee_fix_value [in GMu.InfrastructureSubst]
subst_ee_fix_term [in GMu.InfrastructureSubst]
subst_commute [in GMu.InfrastructureSubst]
subst_tb_many_id_on_fresh_env [in GMu.InfrastructureSubst]
subst_tt_many_id_on_fresh [in GMu.InfrastructureSubst]
subst_tb_id_on_fresh [in GMu.InfrastructureSubst]
subst_te_many_commutes_open [in GMu.InfrastructureSubst]
subst_tt_many_free [in GMu.InfrastructureSubst]
subst_te_intro_many [in GMu.InfrastructureSubst]
subst_intro_commutes_opens_te [in GMu.InfrastructureSubst]
subst_commutes_with_unrelated_opens_te [in GMu.InfrastructureSubst]
subst_commutes_open_tt_many [in GMu.InfrastructureSubst]
subst_removes_var [in GMu.InfrastructureSubst]
subst_idempotent_through_many_open [in GMu.InfrastructureSubst]
subst_idempotent [in GMu.InfrastructureSubst]
subst_ee_value [in GMu.InfrastructureSubst]
subst_ee_term [in GMu.InfrastructureSubst]
subst_te_value [in GMu.InfrastructureSubst]
subst_te_term [in GMu.InfrastructureSubst]
subst_commutes_with_unrelated_opens_te_ee [in GMu.InfrastructureSubst]
subst_commutes_with_unrelated_opens_te_te [in GMu.InfrastructureSubst]
subst_tt_type [in GMu.InfrastructureSubst]
subst_map_reverse_type [in GMu.InfrastructureSubst]
subst_ee_open_te_var [in GMu.InfrastructureSubst]
subst_te_open_ee_var [in GMu.InfrastructureSubst]
subst_ee_intro [in GMu.InfrastructureSubst]
subst_ee_open_ee_var [in GMu.InfrastructureSubst]
subst_ee_open_ee [in GMu.InfrastructureSubst]
subst_ee_fresh [in GMu.InfrastructureSubst]
subst_te_intro [in GMu.InfrastructureSubst]
subst_te_open_te_var [in GMu.InfrastructureSubst]
subst_te_open_te [in GMu.InfrastructureSubst]
subst_te_fresh [in GMu.InfrastructureSubst]
subst_tt_intro_many [in GMu.InfrastructureSubst]
subst_intro_commutes_opens [in GMu.InfrastructureSubst]
subst_commutes_with_unrelated_opens [in GMu.InfrastructureSubst]
subst_tt_intro [in GMu.InfrastructureSubst]
subst_tt_open_tt_var [in GMu.InfrastructureSubst]
subst_tt_open_tt [in GMu.InfrastructureSubst]
subst_tt_open_tt_rec [in GMu.InfrastructureSubst]
subst_tt_fresh [in GMu.InfrastructureSubst]
subst_td_alphas [in GMu.InfrastructureFV]
subst_src_app [in GMu.InfrastructureFV]
subst_match_notin_srcs2 [in GMu.InfrastructureFV]
subst_ttprim_open_tt [in GMu.InfrastructureSubstPrim]
subst_tt_prime_reduce_typ_unit [in GMu.InfrastructureSubstPrim]
subst_tt_prime_reduce_typ_gadt [in GMu.InfrastructureSubstPrim]
subst_tt_prime_reduce_arrow [in GMu.InfrastructureSubstPrim]
subst_tt_prime_reduce_tuple [in GMu.InfrastructureSubstPrim]
subst_tt_prime_reduce_typ_all [in GMu.InfrastructureSubstPrim]
subst_tt_inside [in GMu.InfrastructureSubstPrim]
subst_ttΘ_fresh [in GMu.InfrastructureSubstPrim]
succ_type [in GMu.Tests2]
symmetry_types [in GMu.TestEquality]

T

teq_open [in GMu.SubstMatch]
teq_axiom [in GMu.Equations]
teq_transitivity [in GMu.Equations]
teq_symmetry [in GMu.Equations]
teq_reflexivity [in GMu.Equations]
term_te_closed [in GMu.InfrastructureOpen]
te_closed_id [in GMu.InfrastructureOpen]
te_opening_te_many_adds [in GMu.InfrastructureOpen]
te_opening_ee_preserves [in GMu.InfrastructureOpen]
te_opening_te_adds_one [in GMu.InfrastructureOpen]
Tgen_from_any [in GMu.Regularity]
transitivity_types [in GMu.TestEquality]
type_from_wft [in GMu.Regularity]
type_closed [in GMu.InfrastructureOpen]
typing_implies_term [in GMu.Regularity]
typing_regular [in GMu.Regularity]
typing_exfalso [in GMu.Equations]
typing_replace_typ [in GMu.Preservation]
typing_replace_typ_gen [in GMu.Preservation]
typing_through_subst_te_many [in GMu.Preservation]
typing_through_subst_te_3 [in GMu.Preservation]
typing_through_subst_te_gen [in GMu.Preservation]
typing_through_subst_ee_fix [in GMu.Preservation]
typing_through_subst_ee_lam [in GMu.Preservation]
typing_weakening [in GMu.Preservation]
typing_weakening_delta_many [in GMu.Preservation]
typing_weakening_delta_many_eq [in GMu.Preservation]
typing_weakening_delta [in GMu.Preservation]
typing_weakening_delta_eq [in GMu.Preservation]

U

union_empty [in GMu.Prelude]
union_distributes [in GMu.Prelude]
union_fold_detach [in GMu.Prelude]
union_distribute [in GMu.Prelude]
uvec2_type [in GMu.TestVector]

V

value_regular [in GMu.Prelude]
value_is_term [in GMu.Prelude]

W

well_formed_id [in GMu.Tests]
well_typed_id [in GMu.Tests]
wft_subst_tb_3 [in GMu.Regularity2]
wft_subst_tb_2 [in GMu.Regularity2]
wft_weaken_simple [in GMu.Regularity2]
wft_subst_matching [in GMu.SubstMatch]
wft_subst_matching_gen [in GMu.SubstMatch]
wft_open_many [in GMu.Regularity]
wft_subst_tb_many [in GMu.Regularity]
wft_open [in GMu.Regularity]
wft_subst_tb [in GMu.Regularity]
wft_weaken [in GMu.Regularity]
wft_type [in GMu.Regularity]
wft_strengthen_typ_many [in GMu.Regularity]
wft_strengthen_equations [in GMu.Regularity]
wft_strengthen_equation [in GMu.Regularity]
wft_strengthen_typ [in GMu.Regularity]
wft_from_env_has_typ [in GMu.Regularity]
wft_gives_fv [in GMu.InfrastructureFV]

Z

zero_type [in GMu.Tests2]
zipWithIsMappedZip [in GMu.Zip]
zip_types [in GMu.TestVector]
zip_swap [in GMu.Zip]

---

Axiom Index

A

all_distinct [in GMu.TestVector]
all_distinct [in GMu.TestEquality]

E

Eq [in GMu.TestEquality]

N

Nat [in GMu.Tests2]

S

Succ [in GMu.TestVector]

V

Vector [in GMu.TestVector]

Z

Zero [in GMu.TestVector]

---

Constructor Index

B

bind_var [in GMu.Definitions]

C

clause [in GMu.Definitions]
closed_term_match [in GMu.InfrastructureOpen]
closed_term_constructor [in GMu.InfrastructureOpen]
closed_trm_let [in GMu.InfrastructureOpen]
closed_trm_fix [in GMu.InfrastructureOpen]
closed_trm_tapp [in GMu.InfrastructureOpen]
closed_trm_tabs [in GMu.InfrastructureOpen]
closed_trm_app [in GMu.InfrastructureOpen]
closed_trm_abs [in GMu.InfrastructureOpen]
closed_trm_tuple [in GMu.InfrastructureOpen]
closed_trm_snd [in GMu.InfrastructureOpen]
closed_trm_fst [in GMu.InfrastructureOpen]
closed_trm_unit [in GMu.InfrastructureOpen]
closed_trm_fvar [in GMu.InfrastructureOpen]
closed_trm_bvar [in GMu.InfrastructureOpen]
closed_typ_gadt [in GMu.InfrastructureOpen]
closed_typ_all [in GMu.InfrastructureOpen]
closed_typ_arrow [in GMu.InfrastructureOpen]
closed_typ_tuple [in GMu.InfrastructureOpen]
closed_typ_unit [in GMu.InfrastructureOpen]
closed_typ_fvar [in GMu.InfrastructureOpen]
closed_typ_bvar [in GMu.InfrastructureOpen]

D

distinctive_cons [in GMu.Definitions]
distinctive_empty [in GMu.Definitions]

E

ered_match [in GMu.Definitions]
ered_let [in GMu.Definitions]
ered_tuple_snd [in GMu.Definitions]
ered_tuple_fst [in GMu.Definitions]
ered_snd [in GMu.Definitions]
ered_fst [in GMu.Definitions]
ered_tapp [in GMu.Definitions]
ered_app_2 [in GMu.Definitions]
ered_constructor [in GMu.Definitions]
ered_app_1 [in GMu.Definitions]
eval_finish [in GMu.TestCommon]
eval_step [in GMu.TestCommon]

F

fix_var [in GMu.Definitions]

L

lam_var [in GMu.Definitions]

M

mkGADT [in GMu.Definitions]
mkGADTconstructor [in GMu.Definitions]
mk_type_equation [in GMu.Definitions]

O

okt_typ [in GMu.Definitions]
okt_empty [in GMu.Definitions]
ok_constr_def [in GMu.Definitions]

R

red_match [in GMu.Definitions]
red_fix [in GMu.Definitions]
red_snd [in GMu.Definitions]
red_fst [in GMu.Definitions]
red_letbeta [in GMu.Definitions]
red_tbeta [in GMu.Definitions]
red_beta [in GMu.Definitions]

T

tc_add_eq [in GMu.Definitions]
tc_add_var [in GMu.Definitions]
tc_empty [in GMu.Definitions]
tc_eq [in GMu.Definitions]
tc_var [in GMu.Definitions]
term_matchgadt [in GMu.Definitions]
term_let [in GMu.Definitions]
term_fix [in GMu.Definitions]
term_tapp [in GMu.Definitions]
term_tabs [in GMu.Definitions]
term_app [in GMu.Definitions]
term_abs [in GMu.Definitions]
term_snd [in GMu.Definitions]
term_fst [in GMu.Definitions]
term_tuple [in GMu.Definitions]
term_unit [in GMu.Definitions]
term_constructor [in GMu.Definitions]
term_var [in GMu.Definitions]
Tgen [in GMu.Definitions]
Treg [in GMu.Definitions]
trm_let [in GMu.Definitions]
trm_matchgadt [in GMu.Definitions]
trm_fix [in GMu.Definitions]
trm_tapp [in GMu.Definitions]
trm_tabs [in GMu.Definitions]
trm_app [in GMu.Definitions]
trm_abs [in GMu.Definitions]
trm_snd [in GMu.Definitions]
trm_fst [in GMu.Definitions]
trm_tuple [in GMu.Definitions]
trm_unit [in GMu.Definitions]
trm_constructor [in GMu.Definitions]
trm_fvar [in GMu.Definitions]
trm_bvar [in GMu.Definitions]
type_gadt [in GMu.Definitions]
type_all [in GMu.Definitions]
type_arrow [in GMu.Definitions]
type_tuple [in GMu.Definitions]
type_unit [in GMu.Definitions]
type_var [in GMu.Definitions]
typing_eq [in GMu.Definitions]
typing_case [in GMu.Definitions]
typing_let [in GMu.Definitions]
typing_fix [in GMu.Definitions]
typing_snd [in GMu.Definitions]
typing_fst [in GMu.Definitions]
typing_tuple [in GMu.Definitions]
typing_tapp [in GMu.Definitions]
typing_tabs [in GMu.Definitions]
typing_app [in GMu.Definitions]
typing_abs [in GMu.Definitions]
typing_cons [in GMu.Definitions]
typing_var [in GMu.Definitions]
typing_unit [in GMu.Definitions]
typ_gadt [in GMu.Definitions]
typ_all [in GMu.Definitions]
typ_arrow [in GMu.Definitions]
typ_tuple [in GMu.Definitions]
typ_unit [in GMu.Definitions]
typ_fvar [in GMu.Definitions]
typ_bvar [in GMu.Definitions]

V

value_gadt [in GMu.Definitions]
value_tuple [in GMu.Definitions]
value_lamvar [in GMu.Definitions]
value_unit [in GMu.Definitions]
value_tabs [in GMu.Definitions]
value_abs [in GMu.Definitions]

W

wft_gadt [in GMu.Definitions]
wft_all [in GMu.Definitions]
wft_tuple [in GMu.Definitions]
wft_arrow [in GMu.Definitions]
wft_var [in GMu.Definitions]
wft_unit [in GMu.Definitions]

---

Inductive Index

B

bind [in GMu.Definitions]

C

Clause [in GMu.Definitions]

D

DistinctList [in GMu.Definitions]

E

evals [in GMu.TestCommon]

O

okConstructorDef [in GMu.Definitions]
okt [in GMu.Definitions]

R

red [in GMu.Definitions]

S

subst_matches_typctx [in GMu.Definitions]

T

term [in GMu.Definitions]
te_closed_in_surroundings [in GMu.InfrastructureOpen]
trm [in GMu.Definitions]
typ [in GMu.Definitions]
typctx_elem [in GMu.Definitions]
type [in GMu.Definitions]
type_equation [in GMu.Definitions]
typing [in GMu.Definitions]
typing_taint [in GMu.Definitions]
typ_closed_in_surroundings [in GMu.InfrastructureOpen]

V

value [in GMu.Definitions]
var_kind [in GMu.Definitions]

W

wft [in GMu.Definitions]

---

Projection Index

C

Cargtype [in GMu.Definitions]
Carity [in GMu.Definitions]
Crettypes [in GMu.Definitions]

T

Tarity [in GMu.Definitions]
Tconstructors [in GMu.Definitions]

---

Section Index

M

ManyTest [in GMu.DefinitionsTests]

S

SimpleEquationProperties [in GMu.Equations]

T

trm_ind' [in GMu.Definitions]
typ_ind' [in GMu.Definitions]

Z

Zip [in GMu.Zip]

---

Definition Index

C

clauseArity [in GMu.Definitions]
clauseTerm [in GMu.Definitions]
coerce_trm [in GMu.TestEquality]
coerce_typ [in GMu.TestEquality]
cons [in GMu.TestVector]
Cons [in GMu.TestVector]
const [in GMu.Tests2]
construct_trm [in GMu.TestEquality]
construct_typ [in GMu.TestEquality]
const_test [in GMu.Tests2]
contradictory_bounds [in GMu.Definitions]
ctx [in GMu.Definitions]

D

destruct_trm [in GMu.TestEquality]
destruct_typ [in GMu.TestEquality]
divergent [in GMu.Tests]
domΔ [in GMu.Definitions]

E

emptyΔ [in GMu.Definitions]
entails_semantic [in GMu.Definitions]
EqDef [in GMu.TestEquality]
equations_from_lists [in GMu.Definitions]

F

four [in GMu.Tests2]
fv_env [in GMu.Definitions]
fv_delta [in GMu.Definitions]
fv_trm [in GMu.Definitions]
fv_typs [in GMu.Definitions]
fv_typ [in GMu.Definitions]

G

GADTConstructor [in GMu.Definitions]
GADTEnv [in GMu.Definitions]
GADTName [in GMu.Definitions]
GS [in GMu.TestVector]
GZ [in GMu.TestVector]

H

head_typ [in GMu.TestVector]
head_trm [in GMu.TestVector]

I

id [in GMu.Tests]
id_app [in GMu.Tests]
id_typ [in GMu.Tests]
is_var_defined [in GMu.Definitions]

L

let_id_app [in GMu.Tests]
loop [in GMu.Tests]

M

map [in GMu.TestVector]
map_clause_trm_trm [in GMu.Definitions]
map_clause_trms [in GMu.Definitions]

N

NatDef [in GMu.Tests2]
natSigma [in GMu.Tests2]
nil [in GMu.TestVector]
Nil [in GMu.TestVector]

O

okGadt [in GMu.Definitions]
one [in GMu.Tests2]
open_te_many_var [in GMu.Definitions]
open_tt_many_var [in GMu.Definitions]
open_te_many [in GMu.Definitions]
open_tt_many [in GMu.Definitions]
open_ee [in GMu.Definitions]
open_te [in GMu.Definitions]
open_tt [in GMu.Definitions]
open_ee_rec [in GMu.Definitions]
open_te_rec [in GMu.Definitions]
open_typlist_rec [in GMu.Definitions]
open_tt_rec [in GMu.Definitions]

P

plus [in GMu.Tests2]
preservation [in GMu.Definitions]
progress [in GMu.Definitions]

R

Refl [in GMu.TestEquality]

S

sigma [in GMu.TestVector]
sigma [in GMu.TestEquality]
substitution [in GMu.Definitions]
substitution_sources [in GMu.Definitions]
subst_td_many [in GMu.Definitions]
subst_td [in GMu.Definitions]
subst_tt' [in GMu.Definitions]
subst_tb_many [in GMu.Definitions]
subst_tt_many [in GMu.Definitions]
subst_tb [in GMu.Definitions]
subst_ee [in GMu.Definitions]
subst_te [in GMu.Definitions]
subst_tt [in GMu.Definitions]
subst_te_many [in GMu.InfrastructureSubst]
succ [in GMu.Tests2]
sum [in GMu.Definitions]
symmetry_trm [in GMu.TestEquality]
symmetry_typ [in GMu.TestEquality]

T

tc_vars [in GMu.Definitions]
transitivity_trm [in GMu.TestEquality]
transitivity_typ [in GMu.TestEquality]
trm_size [in GMu.Definitions]
trm_ind' [in GMu.Definitions]
two [in GMu.TestVector]
two [in GMu.Tests2]
typctx [in GMu.Definitions]
typ_size [in GMu.Definitions]
typ_ind' [in GMu.Definitions]

U

uvec2 [in GMu.TestVector]

V

VectorDef [in GMu.TestVector]

Z

zero [in GMu.Tests2]
zip [in GMu.Zip]
zipWith [in GMu.Zip]
zip_typ [in GMu.TestVector]
zip_trm [in GMu.TestVector]

---

Record Index

G

GADTConstructorDef [in GMu.Definitions]
GADTDef [in GMu.Definitions]

---

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

(2881 entries)

Notation 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

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

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

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

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

_

other

(332 entries)

Axiom 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

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

(21 entries)

Projection 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)

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

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

_

other

(98 entries)

Record 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

(2 entries)