| 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 | (2362 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 | (27 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 | (1910 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 | (17 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 | (16 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 | (86 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 | (276 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 | (8 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 | (3 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 | (19 entries) |
Global Index
A
acc:149 [binder, in GMuAnnot.Prelude]acc:151 [binder, in GMuAnnot.Prelude]
acc:153 [binder, in GMuAnnot.Prelude]
acc:155 [binder, in GMuAnnot.Prelude]
acc:20 [binder, in GMuAnnot.Equations]
acc:22 [binder, in GMuAnnot.Equations]
acc:24 [binder, in GMuAnnot.Equations]
acc:26 [binder, in GMuAnnot.Equations]
Ah:132 [binder, in GMuAnnot.Prelude]
Alphas:106 [binder, in GMuAnnot.Regularity]
Alphas:155 [binder, in GMuAnnot.Definitions]
Alphas:302 [binder, in GMuAnnot.Definitions]
Alphas:75 [binder, in GMuAnnot.Prelude]
args:103 [binder, in GMuAnnot.Definitions]
args:99 [binder, in GMuAnnot.Definitions]
As:119 [binder, in GMuAnnot.InfrastructureFV]
As:128 [binder, in GMuAnnot.InfrastructureOpen]
As:138 [binder, in GMuAnnot.Preservation]
As:140 [binder, in GMuAnnot.InfrastructureOpen]
As:153 [binder, in GMuAnnot.InfrastructureFV]
As:158 [binder, in GMuAnnot.InfrastructureSubst]
As:162 [binder, in GMuAnnot.InfrastructureSubst]
As:162 [binder, in GMuAnnot.InfrastructureFV]
As:169 [binder, in GMuAnnot.InfrastructureFV]
As:172 [binder, in GMuAnnot.InfrastructureSubst]
As:176 [binder, in GMuAnnot.InfrastructureSubst]
As:181 [binder, in GMuAnnot.InfrastructureFV]
As:197 [binder, in GMuAnnot.Preservation]
As:209 [binder, in GMuAnnot.SubstMatch]
As:27 [binder, in GMuAnnot.Equations]
As:29 [binder, in GMuAnnot.Preservation]
As:29 [binder, in GMuAnnot.Regularity2]
As:30 [binder, in GMuAnnot.Equations]
As:35 [binder, in GMuAnnot.Equations]
As:35 [binder, in GMuAnnot.Regularity]
As:69 [binder, in GMuAnnot.InfrastructureFV]
As:96 [binder, in GMuAnnot.InfrastructureOpen]
As:96 [binder, in GMuAnnot.Prelude]
As:99 [binder, in GMuAnnot.Regularity]
Ats:133 [binder, in GMuAnnot.Prelude]
A:1 [binder, in GMuAnnot.InfrastructureFV]
A:105 [binder, in GMuAnnot.SubstMatch]
A:107 [binder, in GMuAnnot.Prelude]
A:109 [binder, in GMuAnnot.Regularity]
A:110 [binder, in GMuAnnot.Regularity]
A:110 [binder, in GMuAnnot.SubstMatch]
A:112 [binder, in GMuAnnot.Prelude]
A:117 [binder, in GMuAnnot.Preservation]
A:118 [binder, in GMuAnnot.Preservation]
a:118 [binder, in GMuAnnot.Prelude]
a:120 [binder, in GMuAnnot.Prelude]
A:122 [binder, in GMuAnnot.Prelude]
A:125 [binder, in GMuAnnot.Regularity]
A:126 [binder, in GMuAnnot.Regularity]
A:129 [binder, in GMuAnnot.Prelude]
A:138 [binder, in GMuAnnot.Prelude]
A:142 [binder, in GMuAnnot.Prelude]
A:146 [binder, in GMuAnnot.Prelude]
A:149 [binder, in GMuAnnot.Preservation]
A:149 [binder, in GMuAnnot.InfrastructureFV]
A:150 [binder, in GMuAnnot.Preservation]
A:151 [binder, in GMuAnnot.Preservation]
A:152 [binder, in GMuAnnot.Preservation]
A:153 [binder, in GMuAnnot.Preservation]
A:154 [binder, in GMuAnnot.InfrastructureFV]
A:155 [binder, in GMuAnnot.Preservation]
A:157 [binder, in GMuAnnot.Definitions]
A:157 [binder, in GMuAnnot.Prelude]
A:160 [binder, in GMuAnnot.Prelude]
A:161 [binder, in GMuAnnot.InfrastructureSubst]
a:165 [binder, in GMuAnnot.Prelude]
A:167 [binder, in GMuAnnot.InfrastructureSubst]
A:167 [binder, in GMuAnnot.InfrastructureFV]
A:172 [binder, in GMuAnnot.Prelude]
A:174 [binder, in GMuAnnot.InfrastructureSubst]
A:176 [binder, in GMuAnnot.Prelude]
A:177 [binder, in GMuAnnot.InfrastructureFV]
A:178 [binder, in GMuAnnot.InfrastructureSubst]
A:181 [binder, in GMuAnnot.InfrastructureSubst]
A:183 [binder, in GMuAnnot.Prelude]
A:20 [binder, in GMuAnnot.InfrastructureFV]
A:200 [binder, in GMuAnnot.Preservation]
A:208 [binder, in GMuAnnot.Preservation]
A:209 [binder, in GMuAnnot.Preservation]
A:233 [binder, in GMuAnnot.SubstMatch]
A:25 [binder, in GMuAnnot.InfrastructureSubstPrim]
A:28 [binder, in GMuAnnot.Equations]
A:30 [binder, in GMuAnnot.InfrastructureSubst]
A:304 [binder, in GMuAnnot.Definitions]
A:31 [binder, in GMuAnnot.Regularity2]
A:32 [binder, in GMuAnnot.Regularity2]
A:33 [binder, in GMuAnnot.Preservation]
A:33 [binder, in GMuAnnot.Regularity2]
A:34 [binder, in GMuAnnot.Equations]
A:34 [binder, in GMuAnnot.Preservation]
A:36 [binder, in GMuAnnot.InfrastructureSubst]
A:38 [binder, in GMuAnnot.Regularity]
A:39 [binder, in GMuAnnot.Equations]
A:4 [binder, in GMuAnnot.InfrastructureSubstPrim]
A:42 [binder, in GMuAnnot.Equations]
A:42 [binder, in GMuAnnot.InfrastructureFV]
A:43 [binder, in GMuAnnot.Preservation]
A:44 [binder, in GMuAnnot.Preservation]
A:44 [binder, in GMuAnnot.Prelude]
A:46 [binder, in GMuAnnot.Equations]
A:48 [binder, in GMuAnnot.Prelude]
A:52 [binder, in GMuAnnot.SubstMatch]
a:53 [binder, in GMuAnnot.Prelude]
A:55 [binder, in GMuAnnot.Prelude]
a:63 [binder, in GMuAnnot.Prelude]
a:65 [binder, in GMuAnnot.Prelude]
A:67 [binder, in GMuAnnot.Prelude]
A:69 [binder, in GMuAnnot.Equations]
A:69 [binder, in GMuAnnot.SubstMatch]
A:70 [binder, in GMuAnnot.Definitions]
A:70 [binder, in GMuAnnot.Prelude]
A:76 [binder, in GMuAnnot.Prelude]
A:77 [binder, in GMuAnnot.Prelude]
a:78 [binder, in GMuAnnot.Prelude]
A:79 [binder, in GMuAnnot.Prelude]
A:80 [binder, in GMuAnnot.Preservation]
A:81 [binder, in GMuAnnot.Preservation]
A:93 [binder, in GMuAnnot.Prelude]
A:98 [binder, in GMuAnnot.Prelude]
A:99 [binder, in GMuAnnot.Prelude]
A:99 [binder, in GMuAnnot.SubstMatch]
B
base:10 [binder, in GMuAnnot.InfrastructureFV]base:15 [binder, in GMuAnnot.InfrastructureFV]
base:25 [binder, in GMuAnnot.InfrastructureFV]
base:31 [binder, in GMuAnnot.InfrastructureFV]
base:39 [binder, in GMuAnnot.InfrastructureFV]
base:5 [binder, in GMuAnnot.InfrastructureFV]
binds_ext [lemma, in GMuAnnot.Prelude]
B:100 [binder, in GMuAnnot.Prelude]
B:100 [binder, in GMuAnnot.SubstMatch]
B:113 [binder, in GMuAnnot.Prelude]
b:119 [binder, in GMuAnnot.Prelude]
b:121 [binder, in GMuAnnot.Prelude]
B:139 [binder, in GMuAnnot.Prelude]
B:143 [binder, in GMuAnnot.Prelude]
B:147 [binder, in GMuAnnot.Prelude]
B:158 [binder, in GMuAnnot.Prelude]
B:161 [binder, in GMuAnnot.Prelude]
B:163 [binder, in GMuAnnot.InfrastructureFV]
b:166 [binder, in GMuAnnot.Prelude]
B:170 [binder, in GMuAnnot.InfrastructureFV]
B:177 [binder, in GMuAnnot.Prelude]
B:40 [binder, in GMuAnnot.Equations]
B:43 [binder, in GMuAnnot.Equations]
B:43 [binder, in GMuAnnot.InfrastructureFV]
B:47 [binder, in GMuAnnot.Equations]
B:49 [binder, in GMuAnnot.Prelude]
B:56 [binder, in GMuAnnot.Prelude]
B:58 [binder, in GMuAnnot.Prelude]
b:64 [binder, in GMuAnnot.Prelude]
b:66 [binder, in GMuAnnot.Prelude]
B:80 [binder, in GMuAnnot.Prelude]
B:94 [binder, in GMuAnnot.Prelude]
C
CanonicalConstructorType [lemma, in GMuAnnot.CanonicalForms]CanonicalConstructorTypeGen [lemma, in GMuAnnot.CanonicalForms]
CanonicalFormAbs [lemma, in GMuAnnot.CanonicalForms]
CanonicalFormGadt [lemma, in GMuAnnot.CanonicalForms]
CanonicalForms [library]
CanonicalFormTAbs [lemma, in GMuAnnot.CanonicalForms]
CanonicalFormTuple [lemma, in GMuAnnot.CanonicalForms]
CanonicalFormUnit [lemma, in GMuAnnot.CanonicalForms]
CargType:202 [binder, in GMuAnnot.Definitions]
CargType:96 [binder, in GMuAnnot.Regularity]
Carity:201 [binder, in GMuAnnot.Definitions]
Carity:340 [binder, in GMuAnnot.Definitions]
Carity:95 [binder, in GMuAnnot.Regularity]
Ce:341 [binder, in GMuAnnot.Definitions]
cid:337 [binder, in GMuAnnot.Definitions]
clArity:5 [binder, in GMuAnnot.Definitions]
clause [constructor, in GMuAnnot.Definitions]
Clause [inductive, in GMuAnnot.Definitions]
clauseArity [definition, in GMuAnnot.Definitions]
Clauses:186 [binder, in GMuAnnot.Prelude]
clauses:45 [binder, in GMuAnnot.Definitions]
clauses:56 [binder, in GMuAnnot.Definitions]
clauseTerm [definition, in GMuAnnot.Definitions]
clause:299 [binder, in GMuAnnot.Definitions]
clause:301 [binder, in GMuAnnot.Definitions]
clause:7 [binder, in GMuAnnot.Progress]
clause:9 [binder, in GMuAnnot.Progress]
clA:189 [binder, in GMuAnnot.Prelude]
closed_term_match [constructor, in GMuAnnot.InfrastructureOpen]
closed_term_constructor [constructor, in GMuAnnot.InfrastructureOpen]
closed_trm_let [constructor, in GMuAnnot.InfrastructureOpen]
closed_trm_fix [constructor, in GMuAnnot.InfrastructureOpen]
closed_trm_tapp [constructor, in GMuAnnot.InfrastructureOpen]
closed_trm_tabs [constructor, in GMuAnnot.InfrastructureOpen]
closed_trm_app [constructor, in GMuAnnot.InfrastructureOpen]
closed_trm_abs [constructor, in GMuAnnot.InfrastructureOpen]
closed_trm_tuple [constructor, in GMuAnnot.InfrastructureOpen]
closed_trm_snd [constructor, in GMuAnnot.InfrastructureOpen]
closed_trm_fst [constructor, in GMuAnnot.InfrastructureOpen]
closed_trm_unit [constructor, in GMuAnnot.InfrastructureOpen]
closed_trm_fvar [constructor, in GMuAnnot.InfrastructureOpen]
closed_trm_bvar [constructor, in GMuAnnot.InfrastructureOpen]
closed_id [lemma, in GMuAnnot.InfrastructureOpen]
closed_typ_gadt [constructor, in GMuAnnot.InfrastructureOpen]
closed_typ_all [constructor, in GMuAnnot.InfrastructureOpen]
closed_typ_arrow [constructor, in GMuAnnot.InfrastructureOpen]
closed_typ_tuple [constructor, in GMuAnnot.InfrastructureOpen]
closed_typ_unit [constructor, in GMuAnnot.InfrastructureOpen]
closed_typ_fvar [constructor, in GMuAnnot.InfrastructureOpen]
closed_typ_bvar [constructor, in GMuAnnot.InfrastructureOpen]
clT:190 [binder, in GMuAnnot.Prelude]
cl:154 [binder, in GMuAnnot.Definitions]
cl:17 [binder, in GMuAnnot.InfrastructureFV]
cl:18 [binder, in GMuAnnot.InfrastructureFV]
cl:188 [binder, in GMuAnnot.Prelude]
cl:19 [binder, in GMuAnnot.InfrastructureFV]
cl:29 [binder, in GMuAnnot.InfrastructureFV]
cl:33 [binder, in GMuAnnot.InfrastructureFV]
cl:34 [binder, in GMuAnnot.InfrastructureFV]
cl:35 [binder, in GMuAnnot.InfrastructureFV]
cl:86 [binder, in GMuAnnot.InfrastructureOpen]
contradictory_env_test [lemma, in GMuAnnot.Equations]
contradictory_env_test_0 [lemma, in GMuAnnot.Equations]
CretTypes:203 [binder, in GMuAnnot.Definitions]
CretTypes:97 [binder, in GMuAnnot.Regularity]
cs:72 [binder, in GMuAnnot.Definitions]
cs:75 [binder, in GMuAnnot.Definitions]
Ctors:200 [binder, in GMuAnnot.Definitions]
Ctors:93 [binder, in GMuAnnot.Regularity]
Ctor:14 [binder, in GMuAnnot.CanonicalForms]
Ctor:197 [binder, in GMuAnnot.Definitions]
Ctor:348 [binder, in GMuAnnot.Definitions]
Ctor:6 [binder, in GMuAnnot.CanonicalForms]
Ctor:94 [binder, in GMuAnnot.Regularity]
C:101 [binder, in GMuAnnot.Prelude]
c:101 [binder, in GMuAnnot.SubstMatch]
c:109 [binder, in GMuAnnot.Definitions]
C:133 [binder, in GMuAnnot.InfrastructureFV]
C:140 [binder, in GMuAnnot.Prelude]
C:159 [binder, in GMuAnnot.Prelude]
C:46 [binder, in GMuAnnot.CanonicalForms]
C:48 [binder, in GMuAnnot.Equations]
c:49 [binder, in GMuAnnot.Definitions]
c:57 [binder, in GMuAnnot.Definitions]
C:57 [binder, in GMuAnnot.Prelude]
c:60 [binder, in GMuAnnot.Definitions]
c:61 [binder, in GMuAnnot.Definitions]
c:63 [binder, in GMuAnnot.Definitions]
c:7 [binder, in GMuAnnot.Definitions]
c:73 [binder, in GMuAnnot.Definitions]
c:76 [binder, in GMuAnnot.Definitions]
C:81 [binder, in GMuAnnot.Prelude]
c:86 [binder, in GMuAnnot.Definitions]
c:9 [binder, in GMuAnnot.Definitions]
c:93 [binder, in GMuAnnot.Definitions]
C:95 [binder, in GMuAnnot.Prelude]
D
Definitions [library]DefinitionsTests [library]
Defs:185 [binder, in GMuAnnot.Prelude]
Defs:296 [binder, in GMuAnnot.Definitions]
def:187 [binder, in GMuAnnot.Prelude]
def:298 [binder, in GMuAnnot.Definitions]
def:300 [binder, in GMuAnnot.Definitions]
def:6 [binder, in GMuAnnot.Progress]
def:8 [binder, in GMuAnnot.Progress]
Deqs:140 [binder, in GMuAnnot.InfrastructureFV]
Deqs:20 [binder, in GMuAnnot.Preservation]
Deqs:22 [binder, in GMuAnnot.Regularity2]
Deqs:29 [binder, in GMuAnnot.Regularity]
distinct_split1 [lemma, in GMuAnnot.InfrastructureFV]
domDelta_subst_td [lemma, in GMuAnnot.InfrastructureFV]
domDelta_app [lemma, in GMuAnnot.InfrastructureFV]
domDelta_in [lemma, in GMuAnnot.InfrastructureFV]
D':89 [binder, in GMuAnnot.SubstMatch]
D1:10 [binder, in GMuAnnot.Regularity2]
D1:11 [binder, in GMuAnnot.Preservation]
D1:11 [binder, in GMuAnnot.SubstMatch]
D1:14 [binder, in GMuAnnot.Regularity]
D1:15 [binder, in GMuAnnot.Regularity2]
D1:151 [binder, in GMuAnnot.InfrastructureFV]
D1:173 [binder, in GMuAnnot.InfrastructureFV]
D1:20 [binder, in GMuAnnot.Regularity2]
D1:23 [binder, in GMuAnnot.Regularity]
D1:230 [binder, in GMuAnnot.SubstMatch]
D1:24 [binder, in GMuAnnot.SubstMatch]
D1:27 [binder, in GMuAnnot.Regularity2]
D1:28 [binder, in GMuAnnot.Regularity]
D1:3 [binder, in GMuAnnot.Preservation]
D1:35 [binder, in GMuAnnot.Regularity2]
D1:35 [binder, in GMuAnnot.SubstMatch]
D1:41 [binder, in GMuAnnot.Regularity2]
D1:41 [binder, in GMuAnnot.SubstMatch]
D1:59 [binder, in GMuAnnot.SubstMatch]
D1:6 [binder, in GMuAnnot.Regularity2]
D1:6 [binder, in GMuAnnot.SubstMatch]
D1:62 [binder, in GMuAnnot.Regularity]
D1:65 [binder, in GMuAnnot.Regularity2]
D1:74 [binder, in GMuAnnot.SubstMatch]
D1:76 [binder, in GMuAnnot.Regularity]
D1:79 [binder, in GMuAnnot.Regularity2]
D1:79 [binder, in GMuAnnot.SubstMatch]
D1:81 [binder, in GMuAnnot.Regularity]
D1:92 [binder, in GMuAnnot.InfrastructureFV]
D1:95 [binder, in GMuAnnot.InfrastructureFV]
D2:11 [binder, in GMuAnnot.Regularity2]
D2:116 [binder, in GMuAnnot.SubstMatch]
D2:12 [binder, in GMuAnnot.Preservation]
D2:12 [binder, in GMuAnnot.SubstMatch]
D2:15 [binder, in GMuAnnot.Regularity]
D2:152 [binder, in GMuAnnot.InfrastructureFV]
D2:16 [binder, in GMuAnnot.Regularity2]
D2:174 [binder, in GMuAnnot.InfrastructureFV]
D2:21 [binder, in GMuAnnot.Regularity2]
D2:232 [binder, in GMuAnnot.SubstMatch]
D2:24 [binder, in GMuAnnot.Regularity]
D2:26 [binder, in GMuAnnot.SubstMatch]
D2:28 [binder, in GMuAnnot.Regularity2]
D2:30 [binder, in GMuAnnot.Regularity]
D2:36 [binder, in GMuAnnot.Regularity2]
D2:37 [binder, in GMuAnnot.SubstMatch]
D2:4 [binder, in GMuAnnot.Preservation]
D2:42 [binder, in GMuAnnot.Regularity2]
D2:42 [binder, in GMuAnnot.SubstMatch]
D2:60 [binder, in GMuAnnot.SubstMatch]
D2:63 [binder, in GMuAnnot.Regularity]
D2:66 [binder, in GMuAnnot.Regularity2]
D2:7 [binder, in GMuAnnot.Regularity2]
D2:7 [binder, in GMuAnnot.SubstMatch]
D2:75 [binder, in GMuAnnot.SubstMatch]
D2:77 [binder, in GMuAnnot.Regularity]
D2:80 [binder, in GMuAnnot.Regularity2]
D2:80 [binder, in GMuAnnot.SubstMatch]
D2:82 [binder, in GMuAnnot.Regularity]
D2:93 [binder, in GMuAnnot.InfrastructureFV]
D2:96 [binder, in GMuAnnot.InfrastructureFV]
D3:32 [binder, in GMuAnnot.SubstMatch]
D3:78 [binder, in GMuAnnot.Regularity]
D4:33 [binder, in GMuAnnot.SubstMatch]
D:167 [binder, in GMuAnnot.Prelude]
d:181 [binder, in GMuAnnot.Prelude]
D:19 [binder, in GMuAnnot.SubstMatch]
D:2 [binder, in GMuAnnot.Regularity2]
D:2 [binder, in GMuAnnot.SubstMatch]
D:224 [binder, in GMuAnnot.SubstMatch]
D:49 [binder, in GMuAnnot.Equations]
D:85 [binder, in GMuAnnot.SubstMatch]
D:90 [binder, in GMuAnnot.SubstMatch]
E
empty_is_not_contradictory [lemma, in GMuAnnot.Equations]empty_inter_implies_notin [lemma, in GMuAnnot.Prelude]
empty_eq_is_equivalent [lemma, in GMuAnnot.Progress]
entails_through_subst [lemma, in GMuAnnot.SubstMatch]
env_map_compose [lemma, in GMuAnnot.Prelude]
Equations [library]
equations_from_lists_map [lemma, in GMuAnnot.Equations]
equations_have_no_dom [lemma, in GMuAnnot.InfrastructureFV]
equations_from_lists_are_equations [lemma, in GMuAnnot.Prelude]
equations_weaken_match [lemma, in GMuAnnot.SubstMatch]
equation_strengthen [lemma, in GMuAnnot.SubstMatch]
equation_weaken_var [lemma, in GMuAnnot.SubstMatch]
equation_weaken_eq [lemma, in GMuAnnot.SubstMatch]
eq_dec_var [lemma, in GMuAnnot.Prelude]
eq:141 [binder, in GMuAnnot.InfrastructureFV]
eq:170 [binder, in GMuAnnot.Prelude]
eq:18 [binder, in GMuAnnot.Regularity2]
eq:24 [binder, in GMuAnnot.Preservation]
eq:24 [binder, in GMuAnnot.Regularity2]
eq:32 [binder, in GMuAnnot.Regularity]
eq:7 [binder, in GMuAnnot.Preservation]
eq:82 [binder, in GMuAnnot.Regularity2]
ered_match [constructor, in GMuAnnot.Definitions]
ered_let [constructor, in GMuAnnot.Definitions]
ered_tuple_snd [constructor, in GMuAnnot.Definitions]
ered_tuple_fst [constructor, in GMuAnnot.Definitions]
ered_snd [constructor, in GMuAnnot.Definitions]
ered_fst [constructor, in GMuAnnot.Definitions]
ered_tapp [constructor, in GMuAnnot.Definitions]
ered_app_2 [constructor, in GMuAnnot.Definitions]
ered_constructor [constructor, in GMuAnnot.Definitions]
ered_app_1 [constructor, in GMuAnnot.Definitions]
exist_alphas [lemma, in GMuAnnot.Prelude]
ext_in_map [lemma, in GMuAnnot.Prelude]
e':27 [binder, in GMuAnnot.InfrastructureFV]
e':317 [binder, in GMuAnnot.Definitions]
e':320 [binder, in GMuAnnot.Definitions]
e':323 [binder, in GMuAnnot.Definitions]
e':334 [binder, in GMuAnnot.Definitions]
e':342 [binder, in GMuAnnot.Definitions]
e':350 [binder, in GMuAnnot.Definitions]
e':358 [binder, in GMuAnnot.Definitions]
e':360 [binder, in GMuAnnot.Definitions]
e':383 [binder, in GMuAnnot.Definitions]
e':388 [binder, in GMuAnnot.Definitions]
E0:106 [binder, in GMuAnnot.Preservation]
E0:112 [binder, in GMuAnnot.Preservation]
E0:57 [binder, in GMuAnnot.Preservation]
E0:63 [binder, in GMuAnnot.Preservation]
E0:69 [binder, in GMuAnnot.Preservation]
E0:75 [binder, in GMuAnnot.Preservation]
E0:83 [binder, in GMuAnnot.Preservation]
E0:89 [binder, in GMuAnnot.Preservation]
e1':345 [binder, in GMuAnnot.Definitions]
e1':355 [binder, in GMuAnnot.Definitions]
e1':363 [binder, in GMuAnnot.Definitions]
e1':373 [binder, in GMuAnnot.Definitions]
e1':377 [binder, in GMuAnnot.Definitions]
e1:115 [binder, in GMuAnnot.InfrastructureSubst]
e1:119 [binder, in GMuAnnot.InfrastructureSubst]
e1:120 [binder, in GMuAnnot.Definitions]
e1:122 [binder, in GMuAnnot.Definitions]
e1:126 [binder, in GMuAnnot.Definitions]
e1:127 [binder, in GMuAnnot.Definitions]
e1:130 [binder, in GMuAnnot.Definitions]
e1:132 [binder, in GMuAnnot.Definitions]
e1:135 [binder, in GMuAnnot.Definitions]
e1:146 [binder, in GMuAnnot.Definitions]
e1:15 [binder, in GMuAnnot.CanonicalForms]
e1:150 [binder, in GMuAnnot.Definitions]
e1:159 [binder, in GMuAnnot.Definitions]
e1:160 [binder, in GMuAnnot.Definitions]
e1:162 [binder, in GMuAnnot.Definitions]
e1:168 [binder, in GMuAnnot.Definitions]
e1:184 [binder, in GMuAnnot.InfrastructureSubst]
e1:187 [binder, in GMuAnnot.InfrastructureSubst]
e1:198 [binder, in GMuAnnot.Definitions]
e1:212 [binder, in GMuAnnot.Definitions]
e1:221 [binder, in GMuAnnot.Definitions]
e1:229 [binder, in GMuAnnot.Definitions]
e1:237 [binder, in GMuAnnot.Definitions]
e1:247 [binder, in GMuAnnot.Definitions]
e1:256 [binder, in GMuAnnot.Definitions]
e1:263 [binder, in GMuAnnot.Definitions]
e1:280 [binder, in GMuAnnot.Definitions]
e1:315 [binder, in GMuAnnot.Definitions]
e1:318 [binder, in GMuAnnot.Definitions]
e1:335 [binder, in GMuAnnot.Definitions]
e1:344 [binder, in GMuAnnot.Definitions]
e1:354 [binder, in GMuAnnot.Definitions]
e1:361 [binder, in GMuAnnot.Definitions]
e1:371 [binder, in GMuAnnot.Definitions]
e1:374 [binder, in GMuAnnot.Definitions]
e1:55 [binder, in GMuAnnot.InfrastructureOpen]
e1:63 [binder, in GMuAnnot.InfrastructureOpen]
e1:7 [binder, in GMuAnnot.CanonicalForms]
e1:74 [binder, in GMuAnnot.InfrastructureOpen]
e2':353 [binder, in GMuAnnot.Definitions]
e2':368 [binder, in GMuAnnot.Definitions]
e2:117 [binder, in GMuAnnot.InfrastructureSubst]
e2:121 [binder, in GMuAnnot.InfrastructureSubst]
e2:123 [binder, in GMuAnnot.Definitions]
e2:133 [binder, in GMuAnnot.Definitions]
e2:147 [binder, in GMuAnnot.Definitions]
e2:163 [binder, in GMuAnnot.Definitions]
e2:186 [binder, in GMuAnnot.InfrastructureSubst]
e2:189 [binder, in GMuAnnot.InfrastructureSubst]
e2:222 [binder, in GMuAnnot.Definitions]
e2:248 [binder, in GMuAnnot.Definitions]
e2:281 [binder, in GMuAnnot.Definitions]
e2:322 [binder, in GMuAnnot.Definitions]
e2:346 [binder, in GMuAnnot.Definitions]
e2:352 [binder, in GMuAnnot.Definitions]
e2:362 [binder, in GMuAnnot.Definitions]
e2:367 [binder, in GMuAnnot.Definitions]
e2:372 [binder, in GMuAnnot.Definitions]
e2:56 [binder, in GMuAnnot.InfrastructureOpen]
e2:64 [binder, in GMuAnnot.InfrastructureOpen]
e2:75 [binder, in GMuAnnot.InfrastructureOpen]
e:1 [binder, in GMuAnnot.InfrastructureOpen]
e:1 [binder, in GMuAnnot.Prelude]
e:100 [binder, in GMuAnnot.Definitions]
e:100 [binder, in GMuAnnot.InfrastructureSubst]
e:100 [binder, in GMuAnnot.InfrastructureOpen]
e:101 [binder, in GMuAnnot.Preservation]
E:102 [binder, in GMuAnnot.Prelude]
e:104 [binder, in GMuAnnot.Definitions]
e:105 [binder, in GMuAnnot.Definitions]
e:105 [binder, in GMuAnnot.InfrastructureSubst]
e:105 [binder, in GMuAnnot.InfrastructureOpen]
e:109 [binder, in GMuAnnot.InfrastructureSubst]
E:111 [binder, in GMuAnnot.Prelude]
e:112 [binder, in GMuAnnot.InfrastructureSubst]
e:115 [binder, in GMuAnnot.InfrastructureOpen]
E:118 [binder, in GMuAnnot.InfrastructureFV]
e:118 [binder, in GMuAnnot.InfrastructureOpen]
E:119 [binder, in GMuAnnot.Regularity]
E:12 [binder, in GMuAnnot.CanonicalForms]
E:12 [binder, in GMuAnnot.Regularity]
E:12 [binder, in GMuAnnot.Regularity2]
e:120 [binder, in GMuAnnot.Regularity]
E:122 [binder, in GMuAnnot.Preservation]
E:122 [binder, in GMuAnnot.InfrastructureFV]
e:123 [binder, in GMuAnnot.InfrastructureOpen]
e:124 [binder, in GMuAnnot.Preservation]
E:129 [binder, in GMuAnnot.Regularity]
E:13 [binder, in GMuAnnot.Preservation]
e:130 [binder, in GMuAnnot.Regularity]
e:131 [binder, in GMuAnnot.InfrastructureOpen]
E:132 [binder, in GMuAnnot.Preservation]
E:132 [binder, in GMuAnnot.InfrastructureFV]
e:133 [binder, in GMuAnnot.InfrastructureOpen]
e:134 [binder, in GMuAnnot.Preservation]
E:135 [binder, in GMuAnnot.Regularity]
e:137 [binder, in GMuAnnot.Regularity]
e:139 [binder, in GMuAnnot.InfrastructureSubst]
E:142 [binder, in GMuAnnot.Preservation]
e:142 [binder, in GMuAnnot.InfrastructureSubst]
e:144 [binder, in GMuAnnot.Preservation]
e:147 [binder, in GMuAnnot.InfrastructureSubst]
e:152 [binder, in GMuAnnot.InfrastructureSubst]
E:158 [binder, in GMuAnnot.Preservation]
e:16 [binder, in GMuAnnot.Prelude]
e:164 [binder, in GMuAnnot.Preservation]
e:164 [binder, in GMuAnnot.InfrastructureSubst]
E:168 [binder, in GMuAnnot.InfrastructureSubst]
E:169 [binder, in GMuAnnot.Preservation]
e:17 [binder, in GMuAnnot.Definitions]
E:17 [binder, in GMuAnnot.Regularity2]
e:17 [binder, in GMuAnnot.Prelude]
e:171 [binder, in GMuAnnot.Definitions]
e:174 [binder, in GMuAnnot.Preservation]
E:175 [binder, in GMuAnnot.InfrastructureSubst]
e:177 [binder, in GMuAnnot.Definitions]
E:180 [binder, in GMuAnnot.Preservation]
e:181 [binder, in GMuAnnot.Preservation]
e:182 [binder, in GMuAnnot.Prelude]
E:184 [binder, in GMuAnnot.Definitions]
E:186 [binder, in GMuAnnot.Definitions]
E:188 [binder, in GMuAnnot.Preservation]
e:189 [binder, in GMuAnnot.Preservation]
E:19 [binder, in GMuAnnot.Preservation]
e:19 [binder, in GMuAnnot.Prelude]
E:192 [binder, in GMuAnnot.Definitions]
E:2 [binder, in GMuAnnot.Regularity]
e:21 [binder, in GMuAnnot.CanonicalForms]
e:21 [binder, in GMuAnnot.Prelude]
E:210 [binder, in GMuAnnot.Definitions]
E:218 [binder, in GMuAnnot.Definitions]
e:22 [binder, in GMuAnnot.InfrastructureFV]
E:223 [binder, in GMuAnnot.SubstMatch]
E:228 [binder, in GMuAnnot.Definitions]
E:23 [binder, in GMuAnnot.Regularity2]
e:23 [binder, in GMuAnnot.Prelude]
E:236 [binder, in GMuAnnot.Definitions]
E:244 [binder, in GMuAnnot.Definitions]
E:253 [binder, in GMuAnnot.Definitions]
e:26 [binder, in GMuAnnot.Prelude]
E:260 [binder, in GMuAnnot.Definitions]
E:268 [binder, in GMuAnnot.Definitions]
e:27 [binder, in GMuAnnot.Definitions]
e:27 [binder, in GMuAnnot.Prelude]
E:277 [binder, in GMuAnnot.Definitions]
e:28 [binder, in GMuAnnot.CanonicalForms]
E:28 [binder, in GMuAnnot.Preservation]
e:28 [binder, in GMuAnnot.Prelude]
E:288 [binder, in GMuAnnot.Definitions]
e:289 [binder, in GMuAnnot.Definitions]
e:29 [binder, in GMuAnnot.Definitions]
E:3 [binder, in GMuAnnot.CanonicalForms]
E:3 [binder, in GMuAnnot.Regularity2]
E:30 [binder, in GMuAnnot.Regularity2]
E:307 [binder, in GMuAnnot.Definitions]
e:31 [binder, in GMuAnnot.Prelude]
e:310 [binder, in GMuAnnot.Definitions]
e:32 [binder, in GMuAnnot.Definitions]
e:32 [binder, in GMuAnnot.Prelude]
e:34 [binder, in GMuAnnot.CanonicalForms]
e:34 [binder, in GMuAnnot.Prelude]
e:349 [binder, in GMuAnnot.Definitions]
e:357 [binder, in GMuAnnot.Definitions]
e:359 [binder, in GMuAnnot.Definitions]
e:36 [binder, in GMuAnnot.Prelude]
e:37 [binder, in GMuAnnot.Definitions]
E:37 [binder, in GMuAnnot.Preservation]
e:38 [binder, in GMuAnnot.Prelude]
e:381 [binder, in GMuAnnot.Definitions]
e:386 [binder, in GMuAnnot.Definitions]
e:39 [binder, in GMuAnnot.Definitions]
e:39 [binder, in GMuAnnot.CanonicalForms]
e:40 [binder, in GMuAnnot.Preservation]
E:41 [binder, in GMuAnnot.Regularity]
e:42 [binder, in GMuAnnot.Definitions]
e:42 [binder, in GMuAnnot.CanonicalForms]
E:44 [binder, in GMuAnnot.Regularity]
e:47 [binder, in GMuAnnot.Definitions]
E:47 [binder, in GMuAnnot.Preservation]
e:48 [binder, in GMuAnnot.InfrastructureFV]
E:48 [binder, in GMuAnnot.Regularity2]
E:5 [binder, in GMuAnnot.Preservation]
e:5 [binder, in GMuAnnot.InfrastructureOpen]
E:50 [binder, in GMuAnnot.Regularity]
e:50 [binder, in GMuAnnot.InfrastructureSubst]
e:50 [binder, in GMuAnnot.InfrastructureFV]
e:51 [binder, in GMuAnnot.InfrastructureSubst]
e:51 [binder, in GMuAnnot.InfrastructureOpen]
e:52 [binder, in GMuAnnot.Preservation]
E:53 [binder, in GMuAnnot.Equations]
e:53 [binder, in GMuAnnot.InfrastructureOpen]
e:54 [binder, in GMuAnnot.Equations]
E:54 [binder, in GMuAnnot.Regularity2]
E:56 [binder, in GMuAnnot.Regularity]
e:58 [binder, in GMuAnnot.InfrastructureSubst]
e:6 [binder, in GMuAnnot.Definitions]
E:6 [binder, in GMuAnnot.Regularity]
E:60 [binder, in GMuAnnot.Equations]
e:60 [binder, in GMuAnnot.InfrastructureOpen]
e:61 [binder, in GMuAnnot.Equations]
e:61 [binder, in GMuAnnot.InfrastructureSubst]
E:64 [binder, in GMuAnnot.Regularity]
e:65 [binder, in GMuAnnot.InfrastructureSubst]
e:66 [binder, in GMuAnnot.InfrastructureOpen]
E:67 [binder, in GMuAnnot.Regularity2]
E:68 [binder, in GMuAnnot.Regularity]
e:68 [binder, in GMuAnnot.InfrastructureOpen]
e:7 [binder, in GMuAnnot.InfrastructureFV]
e:71 [binder, in GMuAnnot.InfrastructureOpen]
E:72 [binder, in GMuAnnot.Regularity2]
e:75 [binder, in GMuAnnot.InfrastructureFV]
e:76 [binder, in GMuAnnot.InfrastructureSubst]
e:78 [binder, in GMuAnnot.Definitions]
e:79 [binder, in GMuAnnot.InfrastructureOpen]
E:8 [binder, in GMuAnnot.Regularity2]
e:80 [binder, in GMuAnnot.InfrastructureSubst]
e:80 [binder, in GMuAnnot.InfrastructureFV]
E:81 [binder, in GMuAnnot.Regularity2]
e:82 [binder, in GMuAnnot.InfrastructureOpen]
E:83 [binder, in GMuAnnot.InfrastructureFV]
e:85 [binder, in GMuAnnot.InfrastructureSubst]
E:87 [binder, in GMuAnnot.InfrastructureFV]
e:87 [binder, in GMuAnnot.InfrastructureOpen]
e:89 [binder, in GMuAnnot.InfrastructureSubst]
e:90 [binder, in GMuAnnot.Definitions]
e:91 [binder, in GMuAnnot.InfrastructureOpen]
E:96 [binder, in GMuAnnot.Preservation]
e:99 [binder, in GMuAnnot.InfrastructureOpen]
F
fold_left_subset [lemma, in GMuAnnot.InfrastructureFV]fold_left_subset_base [lemma, in GMuAnnot.InfrastructureFV]
fold_empty [lemma, in GMuAnnot.InfrastructureFV]
Forall2_eq_len [lemma, in GMuAnnot.Prelude]
from_list_spec2 [lemma, in GMuAnnot.Prelude]
from_list_spec [lemma, in GMuAnnot.Prelude]
fv_trm [definition, in GMuAnnot.Definitions]
fv_delta_equations [lemma, in GMuAnnot.InfrastructureFV]
fv_delta_alphas [lemma, in GMuAnnot.InfrastructureFV]
fv_delta_app [lemma, in GMuAnnot.InfrastructureFV]
fv_env_subst [lemma, in GMuAnnot.InfrastructureFV]
fv_subst_tt [lemma, in GMuAnnot.InfrastructureFV]
fv_env_extend [lemma, in GMuAnnot.InfrastructureFV]
fv_open_te_many [lemma, in GMuAnnot.InfrastructureFV]
fv_open_te [lemma, in GMuAnnot.InfrastructureFV]
fv_open_tt [lemma, in GMuAnnot.InfrastructureFV]
fv_smaller_many [lemma, in GMuAnnot.InfrastructureFV]
fv_typs_notin [lemma, in GMuAnnot.InfrastructureFV]
fv_smaller [lemma, in GMuAnnot.InfrastructureFV]
fv_open [lemma, in GMuAnnot.InfrastructureFV]
fv_fold_in [lemma, in GMuAnnot.InfrastructureFV]
fv_fold_in_clause [lemma, in GMuAnnot.InfrastructureFV]
fv_fold_in_general [lemma, in GMuAnnot.InfrastructureFV]
fv_fold_base_clause [lemma, in GMuAnnot.InfrastructureFV]
fv_fold_base [lemma, in GMuAnnot.InfrastructureFV]
fv_fold_general [lemma, in GMuAnnot.InfrastructureFV]
fv:100 [binder, in GMuAnnot.InfrastructureFV]
fv:108 [binder, in GMuAnnot.Definitions]
fv:108 [binder, in GMuAnnot.InfrastructureFV]
fv:11 [binder, in GMuAnnot.InfrastructureFV]
fv:110 [binder, in GMuAnnot.Definitions]
fv:135 [binder, in GMuAnnot.InfrastructureFV]
fv:16 [binder, in GMuAnnot.InfrastructureFV]
fv:164 [binder, in GMuAnnot.InfrastructureFV]
fv:171 [binder, in GMuAnnot.InfrastructureFV]
fv:26 [binder, in GMuAnnot.InfrastructureFV]
fv:32 [binder, in GMuAnnot.InfrastructureFV]
fv:40 [binder, in GMuAnnot.InfrastructureFV]
fv:49 [binder, in GMuAnnot.InfrastructureFV]
fv:6 [binder, in GMuAnnot.InfrastructureFV]
F0:107 [binder, in GMuAnnot.Preservation]
F0:113 [binder, in GMuAnnot.Preservation]
F0:19 [binder, in GMuAnnot.Regularity]
F0:21 [binder, in GMuAnnot.Regularity]
F0:58 [binder, in GMuAnnot.Preservation]
F0:64 [binder, in GMuAnnot.Preservation]
F0:70 [binder, in GMuAnnot.Preservation]
F0:76 [binder, in GMuAnnot.Preservation]
F0:84 [binder, in GMuAnnot.Preservation]
F0:90 [binder, in GMuAnnot.Preservation]
F1:95 [binder, in GMuAnnot.Equations]
F2:96 [binder, in GMuAnnot.Equations]
f:103 [binder, in GMuAnnot.Prelude]
f:115 [binder, in GMuAnnot.Prelude]
f:128 [binder, in GMuAnnot.Prelude]
F:136 [binder, in GMuAnnot.Prelude]
F:143 [binder, in GMuAnnot.Preservation]
F:159 [binder, in GMuAnnot.Preservation]
f:162 [binder, in GMuAnnot.Prelude]
F:178 [binder, in GMuAnnot.Prelude]
F:184 [binder, in GMuAnnot.Prelude]
F:38 [binder, in GMuAnnot.Preservation]
F:4 [binder, in GMuAnnot.Regularity2]
f:45 [binder, in GMuAnnot.Prelude]
F:48 [binder, in GMuAnnot.Preservation]
f:50 [binder, in GMuAnnot.Prelude]
F:55 [binder, in GMuAnnot.Regularity2]
F:60 [binder, in GMuAnnot.Regularity]
f:71 [binder, in GMuAnnot.Definitions]
F:73 [binder, in GMuAnnot.Regularity2]
f:74 [binder, in GMuAnnot.Definitions]
f:82 [binder, in GMuAnnot.Prelude]
F:94 [binder, in GMuAnnot.Equations]
F:97 [binder, in GMuAnnot.Preservation]
G
GADTC:19 [binder, in GMuAnnot.Definitions]gadt_constructor_ok [lemma, in GMuAnnot.Regularity]
GTs:136 [binder, in GMuAnnot.InfrastructureOpen]
g:104 [binder, in GMuAnnot.Prelude]
g:116 [binder, in GMuAnnot.Prelude]
G:151 [binder, in GMuAnnot.Definitions]
G:336 [binder, in GMuAnnot.Definitions]
G:375 [binder, in GMuAnnot.Definitions]
G:39 [binder, in GMuAnnot.Preservation]
G:46 [binder, in GMuAnnot.Definitions]
g:51 [binder, in GMuAnnot.Prelude]
G:81 [binder, in GMuAnnot.InfrastructureOpen]
g:83 [binder, in GMuAnnot.Prelude]
H
head_proof:62 [binder, in GMuAnnot.Definitions]helper_equations_commute [lemma, in GMuAnnot.Preservation]
h:105 [binder, in GMuAnnot.Prelude]
I
Infrastructure [library]InfrastructureFV [library]
InfrastructureOpen [library]
InfrastructureSubst [library]
InfrastructureSubstPrim [library]
inversion_eq_typ_gadt [lemma, in GMuAnnot.Equations]
inversion_eq_typ_all [lemma, in GMuAnnot.Equations]
inversion_eq_tuple [lemma, in GMuAnnot.Equations]
inversion_eq_arrow [lemma, in GMuAnnot.Equations]
inversion_typing_eq [lemma, in GMuAnnot.Equations]
inzip_map_clause_trm [lemma, in GMuAnnot.Prelude]
in_fold_exists [lemma, in GMuAnnot.InfrastructureFV]
in_domΔ_eq [lemma, in GMuAnnot.InfrastructureFV]
in_from_list [lemma, in GMuAnnot.Prelude]
is_var_defined_split [lemma, in GMuAnnot.SubstMatch]
is_var_defined_dom [lemma, in GMuAnnot.SubstMatch]
i:122 [binder, in GMuAnnot.InfrastructureOpen]
i:127 [binder, in GMuAnnot.InfrastructureOpen]
i:45 [binder, in GMuAnnot.InfrastructureOpen]
J
JMeq_from_eq [lemma, in GMuAnnot.Prelude]j:119 [binder, in GMuAnnot.InfrastructureOpen]
j:124 [binder, in GMuAnnot.InfrastructureOpen]
J:15 [binder, in GMuAnnot.InfrastructureOpen]
K
k:108 [binder, in GMuAnnot.InfrastructureSubst]k:108 [binder, in GMuAnnot.InfrastructureOpen]
k:111 [binder, in GMuAnnot.InfrastructureOpen]
k:114 [binder, in GMuAnnot.InfrastructureOpen]
k:117 [binder, in GMuAnnot.InfrastructureOpen]
k:118 [binder, in GMuAnnot.InfrastructureSubst]
k:12 [binder, in GMuAnnot.Prelude]
k:122 [binder, in GMuAnnot.InfrastructureSubst]
k:129 [binder, in GMuAnnot.InfrastructureOpen]
k:134 [binder, in GMuAnnot.InfrastructureOpen]
k:14 [binder, in GMuAnnot.Definitions]
k:16 [binder, in GMuAnnot.InfrastructureOpen]
k:175 [binder, in GMuAnnot.Definitions]
k:18 [binder, in GMuAnnot.InfrastructureOpen]
k:19 [binder, in GMuAnnot.InfrastructureOpen]
k:22 [binder, in GMuAnnot.InfrastructureOpen]
k:25 [binder, in GMuAnnot.InfrastructureOpen]
k:27 [binder, in GMuAnnot.InfrastructureOpen]
k:30 [binder, in GMuAnnot.InfrastructureOpen]
k:33 [binder, in GMuAnnot.InfrastructureOpen]
k:39 [binder, in GMuAnnot.InfrastructureOpen]
k:42 [binder, in GMuAnnot.InfrastructureOpen]
k:46 [binder, in GMuAnnot.InfrastructureOpen]
k:49 [binder, in GMuAnnot.InfrastructureOpen]
k:50 [binder, in GMuAnnot.InfrastructureOpen]
k:52 [binder, in GMuAnnot.InfrastructureOpen]
k:53 [binder, in GMuAnnot.InfrastructureFV]
k:54 [binder, in GMuAnnot.InfrastructureOpen]
k:56 [binder, in GMuAnnot.InfrastructureFV]
k:59 [binder, in GMuAnnot.InfrastructureFV]
k:59 [binder, in GMuAnnot.InfrastructureOpen]
k:62 [binder, in GMuAnnot.InfrastructureFV]
k:62 [binder, in GMuAnnot.InfrastructureOpen]
k:63 [binder, in GMuAnnot.InfrastructureSubst]
k:65 [binder, in GMuAnnot.InfrastructureOpen]
k:67 [binder, in GMuAnnot.InfrastructureOpen]
k:69 [binder, in GMuAnnot.InfrastructureSubst]
k:70 [binder, in GMuAnnot.InfrastructureOpen]
k:73 [binder, in GMuAnnot.InfrastructureOpen]
k:74 [binder, in GMuAnnot.InfrastructureSubst]
k:74 [binder, in GMuAnnot.InfrastructureFV]
k:76 [binder, in GMuAnnot.InfrastructureFV]
k:76 [binder, in GMuAnnot.InfrastructureOpen]
k:80 [binder, in GMuAnnot.InfrastructureOpen]
k:81 [binder, in GMuAnnot.Definitions]
k:84 [binder, in GMuAnnot.InfrastructureOpen]
k:87 [binder, in GMuAnnot.InfrastructureSubst]
k:88 [binder, in GMuAnnot.Definitions]
k:89 [binder, in GMuAnnot.InfrastructureOpen]
k:94 [binder, in GMuAnnot.InfrastructureOpen]
L
la:163 [binder, in GMuAnnot.Prelude]lb:164 [binder, in GMuAnnot.Prelude]
length_equality [lemma, in GMuAnnot.Prelude]
len:74 [binder, in GMuAnnot.Prelude]
LibList_mem [lemma, in GMuAnnot.Prelude]
LibList_map [lemma, in GMuAnnot.Prelude]
lists_map_eq [lemma, in GMuAnnot.Prelude]
list_clause_ind:65 [binder, in GMuAnnot.Definitions]
list_fold_map [lemma, in GMuAnnot.Prelude]
ls:105 [binder, in GMuAnnot.InfrastructureFV]
ls:114 [binder, in GMuAnnot.Prelude]
ls:14 [binder, in GMuAnnot.InfrastructureFV]
ls:24 [binder, in GMuAnnot.InfrastructureFV]
ls:3 [binder, in GMuAnnot.InfrastructureFV]
ls:30 [binder, in GMuAnnot.InfrastructureFV]
ls:38 [binder, in GMuAnnot.InfrastructureFV]
ls:44 [binder, in GMuAnnot.InfrastructureFV]
ls:46 [binder, in GMuAnnot.Prelude]
ls:59 [binder, in GMuAnnot.Prelude]
ls:67 [binder, in GMuAnnot.Definitions]
ls:9 [binder, in GMuAnnot.InfrastructureFV]
l1:174 [binder, in GMuAnnot.Prelude]
l2:175 [binder, in GMuAnnot.Prelude]
l:127 [binder, in GMuAnnot.Prelude]
L:128 [binder, in GMuAnnot.Definitions]
L:131 [binder, in GMuAnnot.Prelude]
L:134 [binder, in GMuAnnot.Definitions]
L:140 [binder, in GMuAnnot.Definitions]
L:145 [binder, in GMuAnnot.Definitions]
L:149 [binder, in GMuAnnot.Definitions]
l:179 [binder, in GMuAnnot.Prelude]
L:207 [binder, in GMuAnnot.Definitions]
L:225 [binder, in GMuAnnot.Definitions]
L:265 [binder, in GMuAnnot.Definitions]
L:274 [binder, in GMuAnnot.Definitions]
L:285 [binder, in GMuAnnot.Definitions]
l:347 [binder, in GMuAnnot.Definitions]
l:52 [binder, in GMuAnnot.Prelude]
L:69 [binder, in GMuAnnot.Prelude]
L:72 [binder, in GMuAnnot.Prelude]
L:73 [binder, in GMuAnnot.Prelude]
l:84 [binder, in GMuAnnot.Prelude]
M
ManyTest [section, in GMuAnnot.DefinitionsTests]ManyTest.T [variable, in GMuAnnot.DefinitionsTests]
map_clause_trm_trm [definition, in GMuAnnot.Definitions]
map_clause_trms [definition, in GMuAnnot.Definitions]
map_map [lemma, in GMuAnnot.Prelude]
map_id [lemma, in GMuAnnot.Prelude]
ms:152 [binder, in GMuAnnot.Definitions]
ms:290 [binder, in GMuAnnot.Definitions]
ms:339 [binder, in GMuAnnot.Definitions]
ms:376 [binder, in GMuAnnot.Definitions]
ms:83 [binder, in GMuAnnot.InfrastructureOpen]
m:11 [binder, in GMuAnnot.Prelude]
N
Name:119 [binder, in GMuAnnot.Definitions]Name:167 [binder, in GMuAnnot.Definitions]
Name:18 [binder, in GMuAnnot.CanonicalForms]
Name:196 [binder, in GMuAnnot.Definitions]
Name:293 [binder, in GMuAnnot.Definitions]
Name:5 [binder, in GMuAnnot.CanonicalForms]
Name:91 [binder, in GMuAnnot.Regularity]
Notations [library]
notin_from_list [lemma, in GMuAnnot.Equations]
notin_fv_wf [lemma, in GMuAnnot.Regularity]
notin_domDelta_subst_td [lemma, in GMuAnnot.InfrastructureFV]
notin_env_binds [lemma, in GMuAnnot.InfrastructureFV]
notin_dom_tc_vars [lemma, in GMuAnnot.InfrastructureFV]
notin_domΔ_eq [lemma, in GMuAnnot.InfrastructureFV]
notin_env_inv [lemma, in GMuAnnot.InfrastructureFV]
notin_fv_tt_open [lemma, in GMuAnnot.InfrastructureFV]
notin_fold [lemma, in GMuAnnot.InfrastructureFV]
notin_inverse [lemma, in GMuAnnot.Prelude]
nth_error_map [lemma, in GMuAnnot.Prelude]
n:10 [binder, in GMuAnnot.InfrastructureOpen]
n:103 [binder, in GMuAnnot.InfrastructureOpen]
n:104 [binder, in GMuAnnot.InfrastructureOpen]
n:107 [binder, in GMuAnnot.InfrastructureOpen]
n:110 [binder, in GMuAnnot.InfrastructureOpen]
n:113 [binder, in GMuAnnot.InfrastructureOpen]
n:12 [binder, in GMuAnnot.Definitions]
n:13 [binder, in GMuAnnot.Prelude]
N:137 [binder, in GMuAnnot.InfrastructureOpen]
n:15 [binder, in GMuAnnot.Prelude]
n:18 [binder, in GMuAnnot.Prelude]
n:180 [binder, in GMuAnnot.Prelude]
N:19 [binder, in GMuAnnot.InfrastructureSubstPrim]
n:20 [binder, in GMuAnnot.Prelude]
n:22 [binder, in GMuAnnot.Prelude]
n:25 [binder, in GMuAnnot.Prelude]
N:29 [binder, in GMuAnnot.InfrastructureOpen]
n:3 [binder, in GMuAnnot.InfrastructureOpen]
n:30 [binder, in GMuAnnot.Prelude]
n:33 [binder, in GMuAnnot.Prelude]
n:34 [binder, in GMuAnnot.InfrastructureOpen]
n:35 [binder, in GMuAnnot.Prelude]
n:37 [binder, in GMuAnnot.Prelude]
n:38 [binder, in GMuAnnot.InfrastructureOpen]
n:40 [binder, in GMuAnnot.Prelude]
N:44 [binder, in GMuAnnot.CanonicalForms]
n:7 [binder, in GMuAnnot.InfrastructureOpen]
N:78 [binder, in GMuAnnot.InfrastructureOpen]
n:8 [binder, in GMuAnnot.InfrastructureSubst]
n:90 [binder, in GMuAnnot.InfrastructureOpen]
N:91 [binder, in GMuAnnot.Equations]
n:95 [binder, in GMuAnnot.InfrastructureOpen]
N:97 [binder, in GMuAnnot.InfrastructureOpen]
n:98 [binder, in GMuAnnot.InfrastructureOpen]
O
okt_is_type [lemma, in GMuAnnot.Regularity]okt_strengthen_delta_var [lemma, in GMuAnnot.Regularity]
okt_strengthen [lemma, in GMuAnnot.Regularity]
okt_is_wft [lemma, in GMuAnnot.Regularity]
okt_push_var_inv [lemma, in GMuAnnot.Regularity]
okt_implies_okgadt [lemma, in GMuAnnot.Regularity]
okt_is_ok [lemma, in GMuAnnot.Regularity]
okt_strengthen_delta_eq [lemma, in GMuAnnot.Regularity2]
okt_replace_typ [lemma, in GMuAnnot.Regularity2]
okt_through_subst_tdtb [lemma, in GMuAnnot.Regularity2]
okt_is_wft_2 [lemma, in GMuAnnot.Regularity2]
okt_push_fresh [lemma, in GMuAnnot.Regularity2]
okt_weakening_delta_many [lemma, in GMuAnnot.Regularity2]
okt_weakening_delta_many_eq [lemma, in GMuAnnot.Regularity2]
okt_weakening_delta_eq [lemma, in GMuAnnot.Regularity2]
okt_weakening_delta [lemma, in GMuAnnot.Regularity2]
okt_strengthen_simple [lemma, in GMuAnnot.Regularity2]
only_vars_is_tc_vars [lemma, in GMuAnnot.Equations]
opening_adds_one [lemma, in GMuAnnot.InfrastructureOpen]
open_te_many_var [definition, in GMuAnnot.Definitions]
open_te_many [definition, in GMuAnnot.Definitions]
open_ee [definition, in GMuAnnot.Definitions]
open_te [definition, in GMuAnnot.Definitions]
open_ee_rec [definition, in GMuAnnot.Definitions]
open_te_rec [definition, in GMuAnnot.Definitions]
open_te_many_test [lemma, in GMuAnnot.DefinitionsTests]
open_tt_many_test [lemma, in GMuAnnot.DefinitionsTests]
open_typlist_test [lemma, in GMuAnnot.DefinitionsTests]
open_ee_test [lemma, in GMuAnnot.DefinitionsTests]
open_te_test [lemma, in GMuAnnot.DefinitionsTests]
open_tt_test [lemma, in GMuAnnot.DefinitionsTests]
open_tt_many_closed [lemma, in GMuAnnot.InfrastructureOpen]
open_ee_rec_term [lemma, in GMuAnnot.InfrastructureOpen]
open_ee_rec_type_many [lemma, in GMuAnnot.InfrastructureOpen]
open_ee_rec_type_core [lemma, in GMuAnnot.InfrastructureOpen]
open_ee_rec_term_core [lemma, in GMuAnnot.InfrastructureOpen]
open_te_rec_term [lemma, in GMuAnnot.InfrastructureOpen]
open_tt_rec_type [lemma, in GMuAnnot.InfrastructureOpen]
open_tt_var_preserves_size [lemma, in GMuAnnot.InfrastructureOpen]
open_te_var_preserves_size [lemma, in GMuAnnot.InfrastructureOpen]
open_ee_var_preserves_size [lemma, in GMuAnnot.InfrastructureOpen]
OTs:135 [binder, in GMuAnnot.InfrastructureOpen]
O1:130 [binder, in GMuAnnot.SubstMatch]
O1:140 [binder, in GMuAnnot.SubstMatch]
O1:146 [binder, in GMuAnnot.InfrastructureFV]
O1:146 [binder, in GMuAnnot.SubstMatch]
O1:160 [binder, in GMuAnnot.SubstMatch]
O1:173 [binder, in GMuAnnot.SubstMatch]
O1:175 [binder, in GMuAnnot.InfrastructureFV]
O1:186 [binder, in GMuAnnot.SubstMatch]
O1:194 [binder, in GMuAnnot.SubstMatch]
O1:20 [binder, in GMuAnnot.SubstMatch]
O1:219 [binder, in GMuAnnot.SubstMatch]
O1:238 [binder, in GMuAnnot.SubstMatch]
O1:27 [binder, in GMuAnnot.SubstMatch]
O1:38 [binder, in GMuAnnot.SubstMatch]
O2:141 [binder, in GMuAnnot.SubstMatch]
O2:147 [binder, in GMuAnnot.InfrastructureFV]
O2:147 [binder, in GMuAnnot.SubstMatch]
O2:174 [binder, in GMuAnnot.SubstMatch]
O2:176 [binder, in GMuAnnot.InfrastructureFV]
O2:187 [binder, in GMuAnnot.SubstMatch]
O2:195 [binder, in GMuAnnot.SubstMatch]
O2:220 [binder, in GMuAnnot.SubstMatch]
O2:239 [binder, in GMuAnnot.SubstMatch]
O2:29 [binder, in GMuAnnot.SubstMatch]
O:103 [binder, in GMuAnnot.SubstMatch]
O:108 [binder, in GMuAnnot.SubstMatch]
O:11 [binder, in GMuAnnot.InfrastructureSubstPrim]
O:114 [binder, in GMuAnnot.SubstMatch]
O:119 [binder, in GMuAnnot.SubstMatch]
O:123 [binder, in GMuAnnot.SubstMatch]
O:14 [binder, in GMuAnnot.InfrastructureSubstPrim]
O:143 [binder, in GMuAnnot.InfrastructureFV]
O:148 [binder, in GMuAnnot.InfrastructureFV]
O:17 [binder, in GMuAnnot.InfrastructureSubstPrim]
O:178 [binder, in GMuAnnot.InfrastructureFV]
O:181 [binder, in GMuAnnot.SubstMatch]
O:193 [binder, in GMuAnnot.SubstMatch]
O:21 [binder, in GMuAnnot.InfrastructureSubstPrim]
O:22 [binder, in GMuAnnot.InfrastructureSubstPrim]
O:231 [binder, in GMuAnnot.SubstMatch]
O:86 [binder, in GMuAnnot.SubstMatch]
O:9 [binder, in GMuAnnot.InfrastructureSubstPrim]
O:93 [binder, in GMuAnnot.SubstMatch]
O:97 [binder, in GMuAnnot.SubstMatch]
P
Ph:134 [binder, in GMuAnnot.Prelude]Prelude [library]
preservation [definition, in GMuAnnot.Definitions]
Preservation [library]
preservation_thm [lemma, in GMuAnnot.Preservation]
progress [definition, in GMuAnnot.Definitions]
Progress [library]
progress_thm [lemma, in GMuAnnot.Progress]
Ps:146 [binder, in GMuAnnot.Preservation]
Ps:173 [binder, in GMuAnnot.InfrastructureSubst]
Ps:177 [binder, in GMuAnnot.InfrastructureSubst]
Pts:135 [binder, in GMuAnnot.Prelude]
P:10 [binder, in GMuAnnot.Prelude]
P:104 [binder, in GMuAnnot.InfrastructureFV]
P:106 [binder, in GMuAnnot.SubstMatch]
P:111 [binder, in GMuAnnot.InfrastructureSubst]
P:111 [binder, in GMuAnnot.SubstMatch]
P:113 [binder, in GMuAnnot.InfrastructureFV]
P:114 [binder, in GMuAnnot.InfrastructureSubst]
P:117 [binder, in GMuAnnot.InfrastructureFV]
P:12 [binder, in GMuAnnot.InfrastructureSubst]
P:125 [binder, in GMuAnnot.Preservation]
P:125 [binder, in GMuAnnot.InfrastructureSubst]
P:129 [binder, in GMuAnnot.InfrastructureSubst]
P:130 [binder, in GMuAnnot.InfrastructureFV]
P:135 [binder, in GMuAnnot.Preservation]
P:135 [binder, in GMuAnnot.InfrastructureSubst]
P:14 [binder, in GMuAnnot.Prelude]
P:148 [binder, in GMuAnnot.Preservation]
P:154 [binder, in GMuAnnot.Preservation]
P:161 [binder, in GMuAnnot.InfrastructureFV]
P:168 [binder, in GMuAnnot.InfrastructureFV]
P:170 [binder, in GMuAnnot.InfrastructureSubst]
P:173 [binder, in GMuAnnot.Prelude]
P:180 [binder, in GMuAnnot.InfrastructureFV]
P:182 [binder, in GMuAnnot.InfrastructureSubst]
P:184 [binder, in GMuAnnot.InfrastructureFV]
P:188 [binder, in GMuAnnot.InfrastructureFV]
P:200 [binder, in GMuAnnot.SubstMatch]
P:23 [binder, in GMuAnnot.InfrastructureFV]
P:24 [binder, in GMuAnnot.Prelude]
P:26 [binder, in GMuAnnot.InfrastructureSubstPrim]
P:29 [binder, in GMuAnnot.Prelude]
P:33 [binder, in GMuAnnot.InfrastructureSubst]
P:38 [binder, in GMuAnnot.Regularity2]
P:39 [binder, in GMuAnnot.InfrastructureSubst]
P:39 [binder, in GMuAnnot.Prelude]
P:4 [binder, in GMuAnnot.InfrastructureFV]
P:44 [binder, in GMuAnnot.Regularity2]
P:47 [binder, in GMuAnnot.InfrastructureFV]
P:5 [binder, in GMuAnnot.InfrastructureSubstPrim]
P:60 [binder, in GMuAnnot.Regularity2]
P:60 [binder, in GMuAnnot.Prelude]
P:69 [binder, in GMuAnnot.Regularity2]
P:7 [binder, in GMuAnnot.InfrastructureSubst]
P:82 [binder, in GMuAnnot.InfrastructureSubst]
P:84 [binder, in GMuAnnot.Regularity]
P:93 [binder, in GMuAnnot.InfrastructureSubst]
P:98 [binder, in GMuAnnot.InfrastructureSubst]
R
red [inductive, in GMuAnnot.Definitions]red_match [constructor, in GMuAnnot.Definitions]
red_fix [constructor, in GMuAnnot.Definitions]
red_snd [constructor, in GMuAnnot.Definitions]
red_fst [constructor, in GMuAnnot.Definitions]
red_letbeta [constructor, in GMuAnnot.Definitions]
red_tbeta [constructor, in GMuAnnot.Definitions]
red_beta [constructor, in GMuAnnot.Definitions]
Regularity [library]
Regularity2 [library]
remove_true_equations [lemma, in GMuAnnot.Preservation]
remove_true_equation [lemma, in GMuAnnot.Preservation]
rewrite_open_tt_many_gadt [lemma, in GMuAnnot.InfrastructureOpen]
S
SimpleEquationProperties [section, in GMuAnnot.Equations]SimpleEquationProperties.Σ [variable, in GMuAnnot.Equations]
sources_list_fst [lemma, in GMuAnnot.InfrastructureFV]
sources_distinct [lemma, in GMuAnnot.SubstMatch]
spawn_unit_subst [lemma, in GMuAnnot.Equations]
split_notin_subset_union [lemma, in GMuAnnot.Prelude]
strong_induction_on_typ_size [lemma, in GMuAnnot.Prelude]
strong_induction_on_type_size_helper [lemma, in GMuAnnot.Prelude]
strong_induction_on_term_size [lemma, in GMuAnnot.Prelude]
strong_induction_on_term_size_helper [lemma, in GMuAnnot.Prelude]
strong_induction [lemma, in GMuAnnot.Prelude]
sublist_head_prop [lemma, in GMuAnnot.InfrastructureSubst]
sublist_tail_prop [lemma, in GMuAnnot.InfrastructureSubst]
subset_fold [lemma, in GMuAnnot.InfrastructureFV]
subset_transitive [lemma, in GMuAnnot.Prelude]
substitution_sources_from_in [lemma, in GMuAnnot.InfrastructureFV]
SubstMatch [library]
subst_ee [definition, in GMuAnnot.Definitions]
subst_te [definition, in GMuAnnot.Definitions]
subst_has_no_fv2 [lemma, in GMuAnnot.Equations]
subst_ttΘ_into_tuple [lemma, in GMuAnnot.Equations]
subst_ttΘ_into_abs [lemma, in GMuAnnot.Equations]
subst_has_no_fv [lemma, in GMuAnnot.Equations]
subst_ee_fix_value [lemma, in GMuAnnot.InfrastructureSubst]
subst_ee_fix_term [lemma, in GMuAnnot.InfrastructureSubst]
subst_commute [lemma, in GMuAnnot.InfrastructureSubst]
subst_tb_many_id_on_fresh_env [lemma, in GMuAnnot.InfrastructureSubst]
subst_tt_many_id_on_fresh [lemma, in GMuAnnot.InfrastructureSubst]
subst_tb_id_on_fresh [lemma, in GMuAnnot.InfrastructureSubst]
subst_te_many_commutes_open [lemma, in GMuAnnot.InfrastructureSubst]
subst_tt_many_free [lemma, in GMuAnnot.InfrastructureSubst]
subst_te_intro_many [lemma, in GMuAnnot.InfrastructureSubst]
subst_intro_commutes_opens_te [lemma, in GMuAnnot.InfrastructureSubst]
subst_commutes_with_unrelated_opens_te [lemma, in GMuAnnot.InfrastructureSubst]
subst_te_many [definition, in GMuAnnot.InfrastructureSubst]
subst_commutes_open_tt_many [lemma, in GMuAnnot.InfrastructureSubst]
subst_removes_var [lemma, in GMuAnnot.InfrastructureSubst]
subst_idempotent_through_many_open [lemma, in GMuAnnot.InfrastructureSubst]
subst_idempotent [lemma, in GMuAnnot.InfrastructureSubst]
subst_ee_value [lemma, in GMuAnnot.InfrastructureSubst]
subst_ee_term [lemma, in GMuAnnot.InfrastructureSubst]
subst_te_value [lemma, in GMuAnnot.InfrastructureSubst]
subst_te_term [lemma, in GMuAnnot.InfrastructureSubst]
subst_commutes_with_unrelated_opens_te_ee [lemma, in GMuAnnot.InfrastructureSubst]
subst_commutes_with_unrelated_opens_te_te [lemma, in GMuAnnot.InfrastructureSubst]
subst_tt_type [lemma, in GMuAnnot.InfrastructureSubst]
subst_map_reverse_type [lemma, in GMuAnnot.InfrastructureSubst]
subst_ee_open_te_var [lemma, in GMuAnnot.InfrastructureSubst]
subst_te_open_ee_var [lemma, in GMuAnnot.InfrastructureSubst]
subst_ee_intro [lemma, in GMuAnnot.InfrastructureSubst]
subst_ee_open_ee_var [lemma, in GMuAnnot.InfrastructureSubst]
subst_ee_open_ee [lemma, in GMuAnnot.InfrastructureSubst]
subst_ee_fresh [lemma, in GMuAnnot.InfrastructureSubst]
subst_te_intro [lemma, in GMuAnnot.InfrastructureSubst]
subst_te_open_te_var [lemma, in GMuAnnot.InfrastructureSubst]
subst_te_open_te [lemma, in GMuAnnot.InfrastructureSubst]
subst_te_fresh [lemma, in GMuAnnot.InfrastructureSubst]
subst_tt_intro_many [lemma, in GMuAnnot.InfrastructureSubst]
subst_intro_commutes_opens [lemma, in GMuAnnot.InfrastructureSubst]
subst_commutes_with_unrelated_opens [lemma, in GMuAnnot.InfrastructureSubst]
subst_tt_intro [lemma, in GMuAnnot.InfrastructureSubst]
subst_tt_open_tt_var [lemma, in GMuAnnot.InfrastructureSubst]
subst_tt_open_tt [lemma, in GMuAnnot.InfrastructureSubst]
subst_tt_open_tt_rec [lemma, in GMuAnnot.InfrastructureSubst]
subst_tt_fresh [lemma, in GMuAnnot.InfrastructureSubst]
subst_td_alphas [lemma, in GMuAnnot.InfrastructureFV]
subst_src_app [lemma, in GMuAnnot.InfrastructureFV]
subst_match_notin_srcs2 [lemma, in GMuAnnot.InfrastructureFV]
subst_td_eqs [lemma, in GMuAnnot.Regularity2]
subst_ttprim_open_tt [lemma, in GMuAnnot.InfrastructureSubstPrim]
subst_tt_prime_reduce_typ_unit [lemma, in GMuAnnot.InfrastructureSubstPrim]
subst_tt_prime_reduce_typ_gadt [lemma, in GMuAnnot.InfrastructureSubstPrim]
subst_tt_prime_reduce_arrow [lemma, in GMuAnnot.InfrastructureSubstPrim]
subst_tt_prime_reduce_tuple [lemma, in GMuAnnot.InfrastructureSubstPrim]
subst_tt_prime_reduce_typ_all [lemma, in GMuAnnot.InfrastructureSubstPrim]
subst_tt_inside [lemma, in GMuAnnot.InfrastructureSubstPrim]
subst_ttΘ_fresh [lemma, in GMuAnnot.InfrastructureSubstPrim]
subst_tb_many_split [lemma, in GMuAnnot.Prelude]
subst_strengthen_true_eq [lemma, in GMuAnnot.SubstMatch]
subst_match_inv_missing_var [lemma, in GMuAnnot.SubstMatch]
subst_eq_weaken2 [lemma, in GMuAnnot.SubstMatch]
subst_match_split [lemma, in GMuAnnot.SubstMatch]
subst_remove_used_var [lemma, in GMuAnnot.SubstMatch]
subst_eq_reorder2 [lemma, in GMuAnnot.SubstMatch]
subst_eq_reorder2_2 [lemma, in GMuAnnot.SubstMatch]
subst_eq_reorder1 [lemma, in GMuAnnot.SubstMatch]
subst_tt_split [lemma, in GMuAnnot.SubstMatch]
subst_eq_reorder1_2 [lemma, in GMuAnnot.SubstMatch]
subst_idempotent_simple [lemma, in GMuAnnot.SubstMatch]
subst_has_closed [lemma, in GMuAnnot.SubstMatch]
subst_has_wft [lemma, in GMuAnnot.SubstMatch]
subst_tt_prime_reduce_typ_fvar_undefined [lemma, in GMuAnnot.SubstMatch]
subst_tt_prime_reduce_typ_fvar_defined [lemma, in GMuAnnot.SubstMatch]
subst_match_remove_right_var3 [lemma, in GMuAnnot.SubstMatch]
subst_match_remove_unused_var [lemma, in GMuAnnot.SubstMatch]
subst_eq_weaken [lemma, in GMuAnnot.SubstMatch]
subst_eq_strengthen_gen [lemma, in GMuAnnot.SubstMatch]
subst_eq_strengthen [lemma, in GMuAnnot.SubstMatch]
subst_match_remove_right_var2 [lemma, in GMuAnnot.SubstMatch]
subst_match_remove_right_var [lemma, in GMuAnnot.SubstMatch]
subst_match_notin_srcs [lemma, in GMuAnnot.SubstMatch]
subst_match_decompose_var [lemma, in GMuAnnot.SubstMatch]
subst_match_remove_eq [lemma, in GMuAnnot.SubstMatch]
subst_sources_from_match [lemma, in GMuAnnot.SubstMatch]
sum [definition, in GMuAnnot.Definitions]
T
tail_proof:64 [binder, in GMuAnnot.Definitions]Targ:204 [binder, in GMuAnnot.Definitions]
Tarity:199 [binder, in GMuAnnot.Definitions]
Tarity:295 [binder, in GMuAnnot.Definitions]
Tarity:92 [binder, in GMuAnnot.Regularity]
TA1:73 [binder, in GMuAnnot.Equations]
TA1:79 [binder, in GMuAnnot.Equations]
TA2:75 [binder, in GMuAnnot.Equations]
TA2:81 [binder, in GMuAnnot.Equations]
TB1:74 [binder, in GMuAnnot.Equations]
TB1:80 [binder, in GMuAnnot.Equations]
TB2:76 [binder, in GMuAnnot.Equations]
TB2:82 [binder, in GMuAnnot.Equations]
Tc:294 [binder, in GMuAnnot.Definitions]
tc:33 [binder, in GMuAnnot.Equations]
Tc:343 [binder, in GMuAnnot.Definitions]
Tc:378 [binder, in GMuAnnot.Definitions]
teq_axiom [lemma, in GMuAnnot.Equations]
teq_transitivity [lemma, in GMuAnnot.Equations]
teq_symmetry [lemma, in GMuAnnot.Equations]
teq_reflexivity [lemma, in GMuAnnot.Equations]
teq_open [lemma, in GMuAnnot.SubstMatch]
term [inductive, in GMuAnnot.Definitions]
term_matchgadt [constructor, in GMuAnnot.Definitions]
term_let [constructor, in GMuAnnot.Definitions]
term_fix [constructor, in GMuAnnot.Definitions]
term_tapp [constructor, in GMuAnnot.Definitions]
term_tabs [constructor, in GMuAnnot.Definitions]
term_app [constructor, in GMuAnnot.Definitions]
term_abs [constructor, in GMuAnnot.Definitions]
term_snd [constructor, in GMuAnnot.Definitions]
term_fst [constructor, in GMuAnnot.Definitions]
term_tuple [constructor, in GMuAnnot.Definitions]
term_unit [constructor, in GMuAnnot.Definitions]
term_constructor [constructor, in GMuAnnot.Definitions]
term_var [constructor, in GMuAnnot.Definitions]
term_te_closed [lemma, in GMuAnnot.InfrastructureOpen]
te_closed_id [lemma, in GMuAnnot.InfrastructureOpen]
te_opening_te_many_adds [lemma, in GMuAnnot.InfrastructureOpen]
te_opening_ee_preserves [lemma, in GMuAnnot.InfrastructureOpen]
te_opening_te_adds_one [lemma, in GMuAnnot.InfrastructureOpen]
te_closed_in_surroundings [inductive, in GMuAnnot.InfrastructureOpen]
Tgen_from_any [lemma, in GMuAnnot.Regularity]
Tparams:118 [binder, in GMuAnnot.Definitions]
Tparams:13 [binder, in GMuAnnot.CanonicalForms]
Tparams:166 [binder, in GMuAnnot.Definitions]
Tparams:4 [binder, in GMuAnnot.CanonicalForms]
Tparams:91 [binder, in GMuAnnot.InfrastructureSubst]
Tparam:121 [binder, in GMuAnnot.Definitions]
Tparam:94 [binder, in GMuAnnot.InfrastructureSubst]
Tparam:95 [binder, in GMuAnnot.InfrastructureSubst]
Tret:205 [binder, in GMuAnnot.Definitions]
trm [inductive, in GMuAnnot.Definitions]
trm_size [definition, in GMuAnnot.Definitions]
trm_ind' [definition, in GMuAnnot.Definitions]
trm_ind'.trm_let_case [variable, in GMuAnnot.Definitions]
trm_ind'.trm_match_case [variable, in GMuAnnot.Definitions]
trm_ind'.trm_fix_case [variable, in GMuAnnot.Definitions]
trm_ind'.trm_tapp_case [variable, in GMuAnnot.Definitions]
trm_ind'.trm_tabs_case [variable, in GMuAnnot.Definitions]
trm_ind'.trm_app_case [variable, in GMuAnnot.Definitions]
trm_ind'.trm_abs_case [variable, in GMuAnnot.Definitions]
trm_ind'.trm_snd_case [variable, in GMuAnnot.Definitions]
trm_ind'.trm_fst_case [variable, in GMuAnnot.Definitions]
trm_ind'.trm_tuple_case [variable, in GMuAnnot.Definitions]
trm_ind'.trm_unit_case [variable, in GMuAnnot.Definitions]
trm_ind'.trm_constructor_case [variable, in GMuAnnot.Definitions]
trm_ind'.trm_fvar_case [variable, in GMuAnnot.Definitions]
trm_ind'.trm_bvar_case [variable, in GMuAnnot.Definitions]
trm_ind'.P [variable, in GMuAnnot.Definitions]
trm_ind' [section, in GMuAnnot.Definitions]
trm_let [constructor, in GMuAnnot.Definitions]
trm_matchgadt [constructor, in GMuAnnot.Definitions]
trm_fix [constructor, in GMuAnnot.Definitions]
trm_tapp [constructor, in GMuAnnot.Definitions]
trm_tabs [constructor, in GMuAnnot.Definitions]
trm_app [constructor, in GMuAnnot.Definitions]
trm_abs [constructor, in GMuAnnot.Definitions]
trm_snd [constructor, in GMuAnnot.Definitions]
trm_fst [constructor, in GMuAnnot.Definitions]
trm_tuple [constructor, in GMuAnnot.Definitions]
trm_unit [constructor, in GMuAnnot.Definitions]
trm_constructor [constructor, in GMuAnnot.Definitions]
trm_fvar [constructor, in GMuAnnot.Definitions]
trm_bvar [constructor, in GMuAnnot.Definitions]
TR:85 [binder, in GMuAnnot.InfrastructureOpen]
Ts':45 [binder, in GMuAnnot.CanonicalForms]
Ts:107 [binder, in GMuAnnot.Regularity]
Ts:133 [binder, in GMuAnnot.InfrastructureSubst]
Ts:155 [binder, in GMuAnnot.InfrastructureFV]
Ts:159 [binder, in GMuAnnot.InfrastructureSubst]
Ts:163 [binder, in GMuAnnot.InfrastructureSubst]
Ts:168 [binder, in GMuAnnot.Prelude]
Ts:18 [binder, in GMuAnnot.Definitions]
Ts:18 [binder, in GMuAnnot.InfrastructureSubstPrim]
Ts:192 [binder, in GMuAnnot.Preservation]
Ts:195 [binder, in GMuAnnot.Definitions]
Ts:196 [binder, in GMuAnnot.Preservation]
Ts:210 [binder, in GMuAnnot.SubstMatch]
Ts:28 [binder, in GMuAnnot.InfrastructureOpen]
Ts:291 [binder, in GMuAnnot.Definitions]
Ts:338 [binder, in GMuAnnot.Definitions]
Ts:43 [binder, in GMuAnnot.CanonicalForms]
Ts:61 [binder, in GMuAnnot.Regularity2]
Ts:63 [binder, in GMuAnnot.InfrastructureFV]
Ts:77 [binder, in GMuAnnot.InfrastructureOpen]
Ts:79 [binder, in GMuAnnot.InfrastructureFV]
Ts:89 [binder, in GMuAnnot.Equations]
Ts:97 [binder, in GMuAnnot.Equations]
Ts:98 [binder, in GMuAnnot.InfrastructureFV]
Tts:126 [binder, in GMuAnnot.InfrastructureSubst]
TT1:103 [binder, in GMuAnnot.Preservation]
TT1:194 [binder, in GMuAnnot.Definitions]
TT1:223 [binder, in GMuAnnot.Definitions]
TT1:249 [binder, in GMuAnnot.Definitions]
TT1:282 [binder, in GMuAnnot.Definitions]
TT1:297 [binder, in GMuAnnot.Definitions]
TT1:54 [binder, in GMuAnnot.Preservation]
TT2:104 [binder, in GMuAnnot.Preservation]
TT2:224 [binder, in GMuAnnot.Definitions]
TT2:250 [binder, in GMuAnnot.Definitions]
TT2:283 [binder, in GMuAnnot.Definitions]
TT2:55 [binder, in GMuAnnot.Preservation]
TT:103 [binder, in GMuAnnot.InfrastructureFV]
TT:122 [binder, in GMuAnnot.Regularity]
TT:127 [binder, in GMuAnnot.Preservation]
TT:132 [binder, in GMuAnnot.Regularity]
TT:136 [binder, in GMuAnnot.Regularity]
TT:137 [binder, in GMuAnnot.Preservation]
TT:147 [binder, in GMuAnnot.Preservation]
TT:16 [binder, in GMuAnnot.Preservation]
TT:163 [binder, in GMuAnnot.Preservation]
TT:173 [binder, in GMuAnnot.Preservation]
TT:182 [binder, in GMuAnnot.Preservation]
TT:190 [binder, in GMuAnnot.Preservation]
TT:214 [binder, in GMuAnnot.Definitions]
TT:23 [binder, in GMuAnnot.Preservation]
TT:231 [binder, in GMuAnnot.Definitions]
TT:241 [binder, in GMuAnnot.Definitions]
TT:257 [binder, in GMuAnnot.Definitions]
TT:264 [binder, in GMuAnnot.Definitions]
TT:271 [binder, in GMuAnnot.Definitions]
TT:311 [binder, in GMuAnnot.Definitions]
TT:32 [binder, in GMuAnnot.Preservation]
TT:379 [binder, in GMuAnnot.Definitions]
TT:384 [binder, in GMuAnnot.Definitions]
TT:42 [binder, in GMuAnnot.Preservation]
TT:57 [binder, in GMuAnnot.Equations]
TT:63 [binder, in GMuAnnot.Equations]
TT:8 [binder, in GMuAnnot.Preservation]
TV:102 [binder, in GMuAnnot.InfrastructureFV]
type_from_wft [lemma, in GMuAnnot.Regularity]
type_closed [lemma, in GMuAnnot.InfrastructureOpen]
typing [inductive, in GMuAnnot.Definitions]
typing_eq [constructor, in GMuAnnot.Definitions]
typing_case [constructor, in GMuAnnot.Definitions]
typing_let [constructor, in GMuAnnot.Definitions]
typing_fix [constructor, in GMuAnnot.Definitions]
typing_snd [constructor, in GMuAnnot.Definitions]
typing_fst [constructor, in GMuAnnot.Definitions]
typing_tuple [constructor, in GMuAnnot.Definitions]
typing_tapp [constructor, in GMuAnnot.Definitions]
typing_tabs [constructor, in GMuAnnot.Definitions]
typing_app [constructor, in GMuAnnot.Definitions]
typing_abs [constructor, in GMuAnnot.Definitions]
typing_cons [constructor, in GMuAnnot.Definitions]
typing_var [constructor, in GMuAnnot.Definitions]
typing_unit [constructor, in GMuAnnot.Definitions]
typing_exfalso [lemma, in GMuAnnot.Equations]
typing_replace_typ [lemma, in GMuAnnot.Preservation]
typing_replace_typ_gen [lemma, in GMuAnnot.Preservation]
typing_through_subst_te_many [lemma, in GMuAnnot.Preservation]
typing_through_subst_te_3 [lemma, in GMuAnnot.Preservation]
typing_through_subst_te_gen [lemma, in GMuAnnot.Preservation]
typing_through_subst_ee_fix [lemma, in GMuAnnot.Preservation]
typing_through_subst_ee_lam [lemma, in GMuAnnot.Preservation]
typing_weakening [lemma, in GMuAnnot.Preservation]
typing_weakening_delta_many [lemma, in GMuAnnot.Preservation]
typing_weakening_delta_many_eq [lemma, in GMuAnnot.Preservation]
typing_weakening_delta [lemma, in GMuAnnot.Preservation]
typing_weakening_delta_eq [lemma, in GMuAnnot.Preservation]
typing_implies_term [lemma, in GMuAnnot.Regularity]
typing_regular [lemma, in GMuAnnot.Regularity]
Typs:17 [binder, in GMuAnnot.CanonicalForms]
Typs:9 [binder, in GMuAnnot.CanonicalForms]
typ_closed_in_surroundings [inductive, in GMuAnnot.InfrastructureOpen]
T':240 [binder, in GMuAnnot.Definitions]
T':64 [binder, in GMuAnnot.Equations]
T1:12 [binder, in GMuAnnot.InfrastructureSubstPrim]
T1:124 [binder, in GMuAnnot.Definitions]
T1:15 [binder, in GMuAnnot.InfrastructureSubstPrim]
T1:162 [binder, in GMuAnnot.Preservation]
T1:164 [binder, in GMuAnnot.Definitions]
T1:172 [binder, in GMuAnnot.Preservation]
T1:20 [binder, in GMuAnnot.InfrastructureOpen]
T1:201 [binder, in GMuAnnot.SubstMatch]
T1:212 [binder, in GMuAnnot.SubstMatch]
T1:213 [binder, in GMuAnnot.Definitions]
T1:216 [binder, in GMuAnnot.SubstMatch]
T1:219 [binder, in GMuAnnot.Definitions]
t1:22 [binder, in GMuAnnot.Definitions]
T1:22 [binder, in GMuAnnot.CanonicalForms]
T1:221 [binder, in GMuAnnot.SubstMatch]
T1:23 [binder, in GMuAnnot.InfrastructureOpen]
T1:230 [binder, in GMuAnnot.Definitions]
T1:238 [binder, in GMuAnnot.Definitions]
T1:24 [binder, in GMuAnnot.Definitions]
T1:245 [binder, in GMuAnnot.Definitions]
T1:247 [binder, in GMuAnnot.SubstMatch]
T1:254 [binder, in GMuAnnot.Definitions]
T1:261 [binder, in GMuAnnot.Definitions]
T1:29 [binder, in GMuAnnot.CanonicalForms]
T1:308 [binder, in GMuAnnot.Definitions]
T1:326 [binder, in GMuAnnot.Definitions]
T1:330 [binder, in GMuAnnot.Definitions]
t1:34 [binder, in GMuAnnot.Definitions]
T1:364 [binder, in GMuAnnot.Definitions]
T1:369 [binder, in GMuAnnot.Definitions]
T1:4 [binder, in GMuAnnot.InfrastructureSubst]
T1:4 [binder, in GMuAnnot.Progress]
T1:43 [binder, in GMuAnnot.SubstMatch]
T1:48 [binder, in GMuAnnot.SubstMatch]
t1:51 [binder, in GMuAnnot.Definitions]
T1:55 [binder, in GMuAnnot.Equations]
T1:57 [binder, in GMuAnnot.InfrastructureOpen]
T1:61 [binder, in GMuAnnot.SubstMatch]
T1:65 [binder, in GMuAnnot.SubstMatch]
t1:66 [binder, in GMuAnnot.InfrastructureSubst]
T1:72 [binder, in GMuAnnot.InfrastructureFV]
T1:76 [binder, in GMuAnnot.Regularity2]
T1:8 [binder, in GMuAnnot.SubstMatch]
T1:82 [binder, in GMuAnnot.SubstMatch]
T1:89 [binder, in GMuAnnot.Regularity]
T1:9 [binder, in GMuAnnot.InfrastructureSubst]
T2:10 [binder, in GMuAnnot.InfrastructureSubst]
T2:125 [binder, in GMuAnnot.Definitions]
T2:13 [binder, in GMuAnnot.InfrastructureSubstPrim]
T2:16 [binder, in GMuAnnot.InfrastructureSubstPrim]
T2:165 [binder, in GMuAnnot.Definitions]
T2:166 [binder, in GMuAnnot.Preservation]
T2:176 [binder, in GMuAnnot.Preservation]
T2:18 [binder, in GMuAnnot.InfrastructureSubst]
T2:202 [binder, in GMuAnnot.SubstMatch]
T2:21 [binder, in GMuAnnot.InfrastructureOpen]
T2:213 [binder, in GMuAnnot.SubstMatch]
T2:217 [binder, in GMuAnnot.SubstMatch]
T2:220 [binder, in GMuAnnot.Definitions]
T2:222 [binder, in GMuAnnot.SubstMatch]
t2:23 [binder, in GMuAnnot.Definitions]
T2:23 [binder, in GMuAnnot.CanonicalForms]
T2:24 [binder, in GMuAnnot.InfrastructureOpen]
T2:246 [binder, in GMuAnnot.Definitions]
T2:248 [binder, in GMuAnnot.SubstMatch]
T2:25 [binder, in GMuAnnot.Definitions]
T2:255 [binder, in GMuAnnot.Definitions]
T2:262 [binder, in GMuAnnot.Definitions]
T2:279 [binder, in GMuAnnot.Definitions]
T2:30 [binder, in GMuAnnot.CanonicalForms]
T2:309 [binder, in GMuAnnot.Definitions]
T2:327 [binder, in GMuAnnot.Definitions]
T2:331 [binder, in GMuAnnot.Definitions]
t2:35 [binder, in GMuAnnot.Definitions]
T2:365 [binder, in GMuAnnot.Definitions]
T2:370 [binder, in GMuAnnot.Definitions]
T2:44 [binder, in GMuAnnot.SubstMatch]
T2:49 [binder, in GMuAnnot.SubstMatch]
T2:5 [binder, in GMuAnnot.InfrastructureSubst]
T2:5 [binder, in GMuAnnot.Progress]
t2:52 [binder, in GMuAnnot.Definitions]
T2:56 [binder, in GMuAnnot.Equations]
T2:58 [binder, in GMuAnnot.InfrastructureOpen]
T2:62 [binder, in GMuAnnot.SubstMatch]
T2:66 [binder, in GMuAnnot.SubstMatch]
t2:67 [binder, in GMuAnnot.InfrastructureSubst]
T2:73 [binder, in GMuAnnot.InfrastructureFV]
T2:77 [binder, in GMuAnnot.Regularity2]
T2:83 [binder, in GMuAnnot.SubstMatch]
T2:9 [binder, in GMuAnnot.SubstMatch]
T:1 [binder, in GMuAnnot.Progress]
T:10 [binder, in GMuAnnot.InfrastructureSubstPrim]
T:101 [binder, in GMuAnnot.InfrastructureFV]
T:102 [binder, in GMuAnnot.Preservation]
T:102 [binder, in GMuAnnot.Regularity]
T:106 [binder, in GMuAnnot.InfrastructureOpen]
T:109 [binder, in GMuAnnot.InfrastructureFV]
T:109 [binder, in GMuAnnot.InfrastructureOpen]
T:110 [binder, in GMuAnnot.InfrastructureFV]
T:111 [binder, in GMuAnnot.Definitions]
T:111 [binder, in GMuAnnot.Regularity]
T:112 [binder, in GMuAnnot.Regularity]
T:112 [binder, in GMuAnnot.InfrastructureOpen]
T:113 [binder, in GMuAnnot.SubstMatch]
T:114 [binder, in GMuAnnot.InfrastructureFV]
T:116 [binder, in GMuAnnot.Regularity]
T:118 [binder, in GMuAnnot.SubstMatch]
T:12 [binder, in GMuAnnot.InfrastructureFV]
T:121 [binder, in GMuAnnot.Regularity]
T:124 [binder, in GMuAnnot.SubstMatch]
T:125 [binder, in GMuAnnot.InfrastructureFV]
T:125 [binder, in GMuAnnot.Prelude]
T:126 [binder, in GMuAnnot.Preservation]
T:128 [binder, in GMuAnnot.InfrastructureFV]
T:130 [binder, in GMuAnnot.InfrastructureSubst]
T:131 [binder, in GMuAnnot.Regularity]
T:136 [binder, in GMuAnnot.Preservation]
T:137 [binder, in GMuAnnot.Prelude]
T:138 [binder, in GMuAnnot.Regularity]
T:138 [binder, in GMuAnnot.InfrastructureOpen]
T:139 [binder, in GMuAnnot.InfrastructureFV]
T:139 [binder, in GMuAnnot.InfrastructureOpen]
T:141 [binder, in GMuAnnot.Definitions]
T:141 [binder, in GMuAnnot.InfrastructureOpen]
T:141 [binder, in GMuAnnot.Prelude]
T:142 [binder, in GMuAnnot.SubstMatch]
T:144 [binder, in GMuAnnot.Prelude]
T:145 [binder, in GMuAnnot.Preservation]
T:150 [binder, in GMuAnnot.InfrastructureFV]
T:153 [binder, in GMuAnnot.Definitions]
T:156 [binder, in GMuAnnot.Prelude]
T:157 [binder, in GMuAnnot.InfrastructureFV]
T:159 [binder, in GMuAnnot.InfrastructureFV]
T:16 [binder, in GMuAnnot.CanonicalForms]
T:16 [binder, in GMuAnnot.InfrastructureSubst]
T:160 [binder, in GMuAnnot.InfrastructureSubst]
T:166 [binder, in GMuAnnot.InfrastructureFV]
T:17 [binder, in GMuAnnot.Equations]
T:17 [binder, in GMuAnnot.Regularity]
T:171 [binder, in GMuAnnot.InfrastructureSubst]
T:183 [binder, in GMuAnnot.Preservation]
T:183 [binder, in GMuAnnot.InfrastructureSubst]
T:190 [binder, in GMuAnnot.Definitions]
t:191 [binder, in GMuAnnot.Prelude]
T:194 [binder, in GMuAnnot.Preservation]
T:2 [binder, in GMuAnnot.InfrastructureSubstPrim]
T:2 [binder, in GMuAnnot.Progress]
T:20 [binder, in GMuAnnot.InfrastructureSubstPrim]
T:201 [binder, in GMuAnnot.Preservation]
T:206 [binder, in GMuAnnot.Definitions]
T:21 [binder, in GMuAnnot.InfrastructureSubst]
T:210 [binder, in GMuAnnot.Preservation]
T:211 [binder, in GMuAnnot.Preservation]
T:212 [binder, in GMuAnnot.Preservation]
T:213 [binder, in GMuAnnot.Preservation]
T:214 [binder, in GMuAnnot.Preservation]
T:215 [binder, in GMuAnnot.Preservation]
T:216 [binder, in GMuAnnot.Preservation]
T:217 [binder, in GMuAnnot.Preservation]
T:218 [binder, in GMuAnnot.Preservation]
T:218 [binder, in GMuAnnot.SubstMatch]
T:219 [binder, in GMuAnnot.Preservation]
T:23 [binder, in GMuAnnot.InfrastructureSubstPrim]
T:234 [binder, in GMuAnnot.SubstMatch]
T:239 [binder, in GMuAnnot.Definitions]
T:26 [binder, in GMuAnnot.Regularity]
T:26 [binder, in GMuAnnot.InfrastructureSubst]
T:26 [binder, in GMuAnnot.InfrastructureOpen]
T:269 [binder, in GMuAnnot.Definitions]
T:292 [binder, in GMuAnnot.Definitions]
T:3 [binder, in GMuAnnot.Equations]
T:3 [binder, in GMuAnnot.Regularity]
T:3 [binder, in GMuAnnot.InfrastructureSubst]
T:31 [binder, in GMuAnnot.Definitions]
T:31 [binder, in GMuAnnot.Regularity]
T:31 [binder, in GMuAnnot.InfrastructureOpen]
T:314 [binder, in GMuAnnot.Definitions]
T:319 [binder, in GMuAnnot.Definitions]
T:332 [binder, in GMuAnnot.Definitions]
T:35 [binder, in GMuAnnot.CanonicalForms]
T:35 [binder, in GMuAnnot.InfrastructureOpen]
T:356 [binder, in GMuAnnot.Definitions]
T:36 [binder, in GMuAnnot.InfrastructureOpen]
T:37 [binder, in GMuAnnot.Regularity]
T:382 [binder, in GMuAnnot.Definitions]
T:387 [binder, in GMuAnnot.Definitions]
T:39 [binder, in GMuAnnot.Regularity2]
T:40 [binder, in GMuAnnot.Definitions]
T:40 [binder, in GMuAnnot.InfrastructureOpen]
T:41 [binder, in GMuAnnot.Preservation]
T:41 [binder, in GMuAnnot.InfrastructureFV]
T:41 [binder, in GMuAnnot.Prelude]
T:42 [binder, in GMuAnnot.InfrastructureSubst]
T:42 [binder, in GMuAnnot.Prelude]
T:43 [binder, in GMuAnnot.Definitions]
T:43 [binder, in GMuAnnot.Prelude]
T:45 [binder, in GMuAnnot.Regularity2]
T:47 [binder, in GMuAnnot.Regularity]
T:48 [binder, in GMuAnnot.Definitions]
T:5 [binder, in GMuAnnot.Equations]
T:51 [binder, in GMuAnnot.InfrastructureFV]
T:51 [binder, in GMuAnnot.Regularity2]
T:51 [binder, in GMuAnnot.SubstMatch]
T:52 [binder, in GMuAnnot.InfrastructureSubst]
T:53 [binder, in GMuAnnot.Preservation]
T:53 [binder, in GMuAnnot.Regularity]
t:54 [binder, in GMuAnnot.Definitions]
T:54 [binder, in GMuAnnot.InfrastructureFV]
T:54 [binder, in GMuAnnot.Prelude]
T:57 [binder, in GMuAnnot.InfrastructureFV]
T:58 [binder, in GMuAnnot.Regularity2]
T:6 [binder, in GMuAnnot.InfrastructureSubstPrim]
T:60 [binder, in GMuAnnot.InfrastructureFV]
T:61 [binder, in GMuAnnot.InfrastructureOpen]
T:62 [binder, in GMuAnnot.Equations]
T:64 [binder, in GMuAnnot.InfrastructureFV]
T:68 [binder, in GMuAnnot.InfrastructureFV]
T:69 [binder, in GMuAnnot.InfrastructureOpen]
T:70 [binder, in GMuAnnot.InfrastructureFV]
T:71 [binder, in GMuAnnot.Regularity]
T:72 [binder, in GMuAnnot.InfrastructureOpen]
T:74 [binder, in GMuAnnot.Regularity]
T:77 [binder, in GMuAnnot.SubstMatch]
T:78 [binder, in GMuAnnot.InfrastructureFV]
T:79 [binder, in GMuAnnot.Regularity]
T:8 [binder, in GMuAnnot.CanonicalForms]
T:8 [binder, in GMuAnnot.Equations]
T:8 [binder, in GMuAnnot.InfrastructureOpen]
T:82 [binder, in GMuAnnot.InfrastructureFV]
t:83 [binder, in GMuAnnot.Definitions]
T:85 [binder, in GMuAnnot.Equations]
T:85 [binder, in GMuAnnot.Regularity]
T:86 [binder, in GMuAnnot.InfrastructureFV]
T:88 [binder, in GMuAnnot.Prelude]
T:91 [binder, in GMuAnnot.InfrastructureFV]
T:91 [binder, in GMuAnnot.Prelude]
T:92 [binder, in GMuAnnot.Equations]
t:95 [binder, in GMuAnnot.Definitions]
T:96 [binder, in GMuAnnot.InfrastructureSubst]
T:96 [binder, in GMuAnnot.SubstMatch]
t:97 [binder, in GMuAnnot.Definitions]
T:99 [binder, in GMuAnnot.Equations]
T:99 [binder, in GMuAnnot.InfrastructureFV]
U
Uh:31 [binder, in GMuAnnot.InfrastructureSubst]Uh:37 [binder, in GMuAnnot.InfrastructureSubst]
union_empty [lemma, in GMuAnnot.Prelude]
union_distributes [lemma, in GMuAnnot.Prelude]
union_fold_detach [lemma, in GMuAnnot.Prelude]
union_distribute [lemma, in GMuAnnot.Prelude]
Us:100 [binder, in GMuAnnot.Regularity]
Us:138 [binder, in GMuAnnot.InfrastructureSubst]
Us:153 [binder, in GMuAnnot.InfrastructureSubst]
Us:156 [binder, in GMuAnnot.InfrastructureFV]
Us:169 [binder, in GMuAnnot.Prelude]
Us:193 [binder, in GMuAnnot.Preservation]
Us:198 [binder, in GMuAnnot.Preservation]
Us:211 [binder, in GMuAnnot.SubstMatch]
Us:43 [binder, in GMuAnnot.InfrastructureSubst]
Us:62 [binder, in GMuAnnot.Regularity2]
Us:90 [binder, in GMuAnnot.Equations]
Us:98 [binder, in GMuAnnot.Equations]
Ut:32 [binder, in GMuAnnot.InfrastructureSubst]
Ut:38 [binder, in GMuAnnot.InfrastructureSubst]
U0:110 [binder, in GMuAnnot.Preservation]
U0:116 [binder, in GMuAnnot.Preservation]
U0:137 [binder, in GMuAnnot.SubstMatch]
U0:139 [binder, in GMuAnnot.SubstMatch]
U0:154 [binder, in GMuAnnot.SubstMatch]
U0:156 [binder, in GMuAnnot.SubstMatch]
U0:167 [binder, in GMuAnnot.SubstMatch]
U0:169 [binder, in GMuAnnot.SubstMatch]
U0:226 [binder, in GMuAnnot.SubstMatch]
U0:228 [binder, in GMuAnnot.SubstMatch]
U0:61 [binder, in GMuAnnot.Preservation]
U0:67 [binder, in GMuAnnot.Preservation]
U0:73 [binder, in GMuAnnot.Preservation]
U0:79 [binder, in GMuAnnot.Preservation]
U0:87 [binder, in GMuAnnot.Preservation]
U0:93 [binder, in GMuAnnot.Preservation]
U1:184 [binder, in GMuAnnot.Preservation]
U1:240 [binder, in GMuAnnot.SubstMatch]
U1:245 [binder, in GMuAnnot.SubstMatch]
U1:45 [binder, in GMuAnnot.SubstMatch]
U2:185 [binder, in GMuAnnot.Preservation]
U2:241 [binder, in GMuAnnot.SubstMatch]
U2:246 [binder, in GMuAnnot.SubstMatch]
U2:46 [binder, in GMuAnnot.SubstMatch]
u:1 [binder, in GMuAnnot.Preservation]
U:100 [binder, in GMuAnnot.Equations]
U:100 [binder, in GMuAnnot.Preservation]
U:103 [binder, in GMuAnnot.Regularity]
U:108 [binder, in GMuAnnot.Regularity]
U:11 [binder, in GMuAnnot.Regularity]
U:116 [binder, in GMuAnnot.InfrastructureOpen]
u:121 [binder, in GMuAnnot.InfrastructureOpen]
U:123 [binder, in GMuAnnot.InfrastructureSubst]
u:126 [binder, in GMuAnnot.InfrastructureOpen]
U:126 [binder, in GMuAnnot.Prelude]
U:126 [binder, in GMuAnnot.SubstMatch]
U:128 [binder, in GMuAnnot.InfrastructureSubst]
U:129 [binder, in GMuAnnot.InfrastructureFV]
U:129 [binder, in GMuAnnot.SubstMatch]
u:130 [binder, in GMuAnnot.InfrastructureOpen]
U:131 [binder, in GMuAnnot.InfrastructureSubst]
u:132 [binder, in GMuAnnot.InfrastructureOpen]
U:135 [binder, in GMuAnnot.SubstMatch]
U:136 [binder, in GMuAnnot.InfrastructureSubst]
U:14 [binder, in GMuAnnot.Preservation]
U:145 [binder, in GMuAnnot.InfrastructureFV]
U:145 [binder, in GMuAnnot.SubstMatch]
U:15 [binder, in GMuAnnot.Equations]
U:15 [binder, in GMuAnnot.InfrastructureSubst]
U:152 [binder, in GMuAnnot.SubstMatch]
U:156 [binder, in GMuAnnot.InfrastructureSubst]
U:157 [binder, in GMuAnnot.InfrastructureSubst]
U:158 [binder, in GMuAnnot.InfrastructureFV]
U:159 [binder, in GMuAnnot.SubstMatch]
U:16 [binder, in GMuAnnot.Regularity]
U:160 [binder, in GMuAnnot.InfrastructureFV]
U:165 [binder, in GMuAnnot.Preservation]
U:165 [binder, in GMuAnnot.SubstMatch]
U:17 [binder, in GMuAnnot.SubstMatch]
U:170 [binder, in GMuAnnot.Definitions]
U:172 [binder, in GMuAnnot.SubstMatch]
U:175 [binder, in GMuAnnot.Preservation]
u:176 [binder, in GMuAnnot.Definitions]
U:179 [binder, in GMuAnnot.SubstMatch]
U:18 [binder, in GMuAnnot.Equations]
U:180 [binder, in GMuAnnot.InfrastructureSubst]
U:189 [binder, in GMuAnnot.SubstMatch]
U:19 [binder, in GMuAnnot.InfrastructureSubst]
U:195 [binder, in GMuAnnot.Preservation]
U:2 [binder, in GMuAnnot.InfrastructureSubst]
U:204 [binder, in GMuAnnot.SubstMatch]
U:206 [binder, in GMuAnnot.SubstMatch]
u:21 [binder, in GMuAnnot.Preservation]
U:22 [binder, in GMuAnnot.Preservation]
U:22 [binder, in GMuAnnot.SubstMatch]
U:24 [binder, in GMuAnnot.InfrastructureSubstPrim]
U:28 [binder, in GMuAnnot.SubstMatch]
u:30 [binder, in GMuAnnot.Preservation]
U:31 [binder, in GMuAnnot.Preservation]
U:34 [binder, in GMuAnnot.InfrastructureSubst]
U:35 [binder, in GMuAnnot.InfrastructureSubst]
U:37 [binder, in GMuAnnot.InfrastructureOpen]
U:39 [binder, in GMuAnnot.SubstMatch]
U:40 [binder, in GMuAnnot.InfrastructureSubst]
U:41 [binder, in GMuAnnot.InfrastructureOpen]
U:46 [binder, in GMuAnnot.InfrastructureSubst]
U:47 [binder, in GMuAnnot.InfrastructureSubst]
U:49 [binder, in GMuAnnot.InfrastructureSubst]
u:50 [binder, in GMuAnnot.Preservation]
U:51 [binder, in GMuAnnot.Preservation]
U:52 [binder, in GMuAnnot.InfrastructureFV]
U:53 [binder, in GMuAnnot.SubstMatch]
U:54 [binder, in GMuAnnot.InfrastructureSubst]
U:55 [binder, in GMuAnnot.InfrastructureFV]
U:57 [binder, in GMuAnnot.InfrastructureSubst]
U:57 [binder, in GMuAnnot.SubstMatch]
U:58 [binder, in GMuAnnot.InfrastructureFV]
U:59 [binder, in GMuAnnot.Regularity]
U:6 [binder, in GMuAnnot.Equations]
U:6 [binder, in GMuAnnot.Preservation]
U:60 [binder, in GMuAnnot.InfrastructureSubst]
U:61 [binder, in GMuAnnot.InfrastructureFV]
U:63 [binder, in GMuAnnot.Regularity2]
u:64 [binder, in GMuAnnot.InfrastructureSubst]
u:68 [binder, in GMuAnnot.InfrastructureSubst]
U:68 [binder, in GMuAnnot.SubstMatch]
U:70 [binder, in GMuAnnot.Equations]
U:70 [binder, in GMuAnnot.SubstMatch]
u:75 [binder, in GMuAnnot.InfrastructureSubst]
u:79 [binder, in GMuAnnot.InfrastructureSubst]
U:8 [binder, in GMuAnnot.InfrastructureSubstPrim]
u:82 [binder, in GMuAnnot.Definitions]
U:86 [binder, in GMuAnnot.Equations]
U:88 [binder, in GMuAnnot.Regularity]
u:88 [binder, in GMuAnnot.InfrastructureSubst]
U:88 [binder, in GMuAnnot.SubstMatch]
u:89 [binder, in GMuAnnot.Definitions]
U:9 [binder, in GMuAnnot.Equations]
u:9 [binder, in GMuAnnot.Preservation]
U:93 [binder, in GMuAnnot.Equations]
U:96 [binder, in GMuAnnot.Definitions]
u:98 [binder, in GMuAnnot.Definitions]
u:99 [binder, in GMuAnnot.Preservation]
V
value [inductive, in GMuAnnot.Definitions]value_gadt [constructor, in GMuAnnot.Definitions]
value_tuple [constructor, in GMuAnnot.Definitions]
value_lamvar [constructor, in GMuAnnot.Definitions]
value_unit [constructor, in GMuAnnot.Definitions]
value_tabs [constructor, in GMuAnnot.Definitions]
value_abs [constructor, in GMuAnnot.Definitions]
value_regular [lemma, in GMuAnnot.Prelude]
value_is_term [lemma, in GMuAnnot.Prelude]
vk0:109 [binder, in GMuAnnot.Preservation]
vk0:115 [binder, in GMuAnnot.Preservation]
vk0:60 [binder, in GMuAnnot.Preservation]
vk0:66 [binder, in GMuAnnot.Preservation]
vk0:72 [binder, in GMuAnnot.Preservation]
vk0:78 [binder, in GMuAnnot.Preservation]
vk0:86 [binder, in GMuAnnot.Preservation]
vk0:92 [binder, in GMuAnnot.Preservation]
vk:10 [binder, in GMuAnnot.Regularity]
vk:116 [binder, in GMuAnnot.Definitions]
vk:124 [binder, in GMuAnnot.InfrastructureFV]
vk:161 [binder, in GMuAnnot.Preservation]
vk:166 [binder, in GMuAnnot.InfrastructureSubst]
vk:171 [binder, in GMuAnnot.Preservation]
vk:189 [binder, in GMuAnnot.Definitions]
vk:4 [binder, in GMuAnnot.InfrastructureOpen]
vk:46 [binder, in GMuAnnot.Regularity]
vk:48 [binder, in GMuAnnot.InfrastructureOpen]
vk:50 [binder, in GMuAnnot.Regularity2]
vk:52 [binder, in GMuAnnot.Regularity]
vk:57 [binder, in GMuAnnot.Regularity2]
vk:58 [binder, in GMuAnnot.Regularity]
vk:70 [binder, in GMuAnnot.Regularity]
vk:71 [binder, in GMuAnnot.InfrastructureSubst]
vk:75 [binder, in GMuAnnot.Regularity2]
vk:77 [binder, in GMuAnnot.InfrastructureSubst]
vk:83 [binder, in GMuAnnot.InfrastructureSubst]
vk:85 [binder, in GMuAnnot.InfrastructureFV]
vk:90 [binder, in GMuAnnot.InfrastructureFV]
vk:93 [binder, in GMuAnnot.InfrastructureOpen]
Vs:199 [binder, in GMuAnnot.Preservation]
v1:109 [binder, in GMuAnnot.Prelude]
V1:132 [binder, in GMuAnnot.SubstMatch]
v1:138 [binder, in GMuAnnot.Definitions]
v1:142 [binder, in GMuAnnot.Definitions]
V1:149 [binder, in GMuAnnot.SubstMatch]
V1:162 [binder, in GMuAnnot.SubstMatch]
V1:176 [binder, in GMuAnnot.SubstMatch]
v1:24 [binder, in GMuAnnot.CanonicalForms]
v1:31 [binder, in GMuAnnot.CanonicalForms]
v1:321 [binder, in GMuAnnot.Definitions]
v1:324 [binder, in GMuAnnot.Definitions]
v1:328 [binder, in GMuAnnot.Definitions]
v1:351 [binder, in GMuAnnot.Definitions]
v1:36 [binder, in GMuAnnot.CanonicalForms]
v1:366 [binder, in GMuAnnot.Definitions]
v2:110 [binder, in GMuAnnot.Prelude]
V2:133 [binder, in GMuAnnot.SubstMatch]
V2:150 [binder, in GMuAnnot.SubstMatch]
V2:163 [binder, in GMuAnnot.SubstMatch]
V2:177 [binder, in GMuAnnot.SubstMatch]
v2:25 [binder, in GMuAnnot.CanonicalForms]
v2:316 [binder, in GMuAnnot.Definitions]
v2:325 [binder, in GMuAnnot.Definitions]
v2:329 [binder, in GMuAnnot.Definitions]
V:10 [binder, in GMuAnnot.Equations]
V:101 [binder, in GMuAnnot.InfrastructureSubst]
v:106 [binder, in GMuAnnot.InfrastructureSubst]
v:120 [binder, in GMuAnnot.InfrastructureOpen]
V:125 [binder, in GMuAnnot.InfrastructureOpen]
V:129 [binder, in GMuAnnot.Definitions]
V:139 [binder, in GMuAnnot.Definitions]
V:143 [binder, in GMuAnnot.InfrastructureSubst]
V:149 [binder, in GMuAnnot.InfrastructureSubst]
V:158 [binder, in GMuAnnot.Definitions]
V:191 [binder, in GMuAnnot.Preservation]
V:211 [binder, in GMuAnnot.Definitions]
V:22 [binder, in GMuAnnot.InfrastructureSubst]
v:270 [binder, in GMuAnnot.Definitions]
V:278 [binder, in GMuAnnot.Definitions]
V:28 [binder, in GMuAnnot.InfrastructureSubst]
V:31 [binder, in GMuAnnot.SubstMatch]
v:333 [binder, in GMuAnnot.Definitions]
v:47 [binder, in GMuAnnot.CanonicalForms]
W
wft_open_many [lemma, in GMuAnnot.Regularity]wft_subst_tb_many [lemma, in GMuAnnot.Regularity]
wft_open [lemma, in GMuAnnot.Regularity]
wft_subst_tb [lemma, in GMuAnnot.Regularity]
wft_weaken [lemma, in GMuAnnot.Regularity]
wft_type [lemma, in GMuAnnot.Regularity]
wft_strengthen_typ_many [lemma, in GMuAnnot.Regularity]
wft_strengthen_equations [lemma, in GMuAnnot.Regularity]
wft_strengthen_equation [lemma, in GMuAnnot.Regularity]
wft_strengthen_typ [lemma, in GMuAnnot.Regularity]
wft_from_env_has_typ [lemma, in GMuAnnot.Regularity]
wft_gives_fv [lemma, in GMuAnnot.InfrastructureFV]
wft_subst_tb_3 [lemma, in GMuAnnot.Regularity2]
wft_subst_tb_2 [lemma, in GMuAnnot.Regularity2]
wft_weaken_simple [lemma, in GMuAnnot.Regularity2]
wft_subst_matching [lemma, in GMuAnnot.SubstMatch]
wft_subst_matching_gen [lemma, in GMuAnnot.SubstMatch]
X
Xs:104 [binder, in GMuAnnot.InfrastructureSubst]Xs:131 [binder, in GMuAnnot.InfrastructureFV]
Xs:137 [binder, in GMuAnnot.InfrastructureSubst]
Xs:141 [binder, in GMuAnnot.InfrastructureSubst]
Xs:146 [binder, in GMuAnnot.InfrastructureSubst]
Xs:151 [binder, in GMuAnnot.InfrastructureSubst]
Xs:20 [binder, in GMuAnnot.InfrastructureSubst]
Xs:25 [binder, in GMuAnnot.InfrastructureSubst]
Xs:41 [binder, in GMuAnnot.InfrastructureSubst]
Xs:99 [binder, in GMuAnnot.InfrastructureSubst]
x0:108 [binder, in GMuAnnot.Preservation]
x0:114 [binder, in GMuAnnot.Preservation]
X0:136 [binder, in GMuAnnot.SubstMatch]
X0:138 [binder, in GMuAnnot.SubstMatch]
X0:153 [binder, in GMuAnnot.SubstMatch]
X0:155 [binder, in GMuAnnot.SubstMatch]
X0:166 [binder, in GMuAnnot.SubstMatch]
X0:168 [binder, in GMuAnnot.SubstMatch]
x0:59 [binder, in GMuAnnot.Preservation]
x0:65 [binder, in GMuAnnot.Preservation]
x0:71 [binder, in GMuAnnot.Preservation]
x0:77 [binder, in GMuAnnot.Preservation]
x0:85 [binder, in GMuAnnot.Preservation]
x0:91 [binder, in GMuAnnot.Preservation]
x:101 [binder, in GMuAnnot.InfrastructureOpen]
x:102 [binder, in GMuAnnot.InfrastructureOpen]
X:103 [binder, in GMuAnnot.InfrastructureSubst]
X:105 [binder, in GMuAnnot.Preservation]
x:106 [binder, in GMuAnnot.Prelude]
X:107 [binder, in GMuAnnot.InfrastructureFV]
x:108 [binder, in GMuAnnot.Prelude]
X:11 [binder, in GMuAnnot.InfrastructureSubst]
x:11 [binder, in GMuAnnot.InfrastructureOpen]
X:111 [binder, in GMuAnnot.Preservation]
X:111 [binder, in GMuAnnot.InfrastructureFV]
X:115 [binder, in GMuAnnot.Regularity]
X:115 [binder, in GMuAnnot.InfrastructureFV]
x:117 [binder, in GMuAnnot.Definitions]
x:12 [binder, in GMuAnnot.InfrastructureOpen]
x:120 [binder, in GMuAnnot.InfrastructureFV]
X:123 [binder, in GMuAnnot.Regularity]
x:123 [binder, in GMuAnnot.InfrastructureFV]
x:123 [binder, in GMuAnnot.Prelude]
X:124 [binder, in GMuAnnot.Regularity]
X:125 [binder, in GMuAnnot.SubstMatch]
X:127 [binder, in GMuAnnot.InfrastructureFV]
X:128 [binder, in GMuAnnot.Preservation]
X:129 [binder, in GMuAnnot.Preservation]
X:13 [binder, in GMuAnnot.InfrastructureSubst]
X:13 [binder, in GMuAnnot.Regularity2]
x:130 [binder, in GMuAnnot.Prelude]
x:131 [binder, in GMuAnnot.Definitions]
X:131 [binder, in GMuAnnot.SubstMatch]
x:134 [binder, in GMuAnnot.InfrastructureFV]
X:134 [binder, in GMuAnnot.SubstMatch]
X:136 [binder, in GMuAnnot.Definitions]
x:136 [binder, in GMuAnnot.InfrastructureFV]
X:137 [binder, in GMuAnnot.Definitions]
X:14 [binder, in GMuAnnot.Equations]
x:143 [binder, in GMuAnnot.Definitions]
x:144 [binder, in GMuAnnot.Definitions]
X:144 [binder, in GMuAnnot.InfrastructureFV]
X:145 [binder, in GMuAnnot.InfrastructureSubst]
x:145 [binder, in GMuAnnot.Prelude]
x:148 [binder, in GMuAnnot.Definitions]
x:148 [binder, in GMuAnnot.Prelude]
X:148 [binder, in GMuAnnot.SubstMatch]
x:15 [binder, in GMuAnnot.Definitions]
X:150 [binder, in GMuAnnot.InfrastructureSubst]
x:150 [binder, in GMuAnnot.Prelude]
X:151 [binder, in GMuAnnot.SubstMatch]
x:152 [binder, in GMuAnnot.Prelude]
X:154 [binder, in GMuAnnot.InfrastructureSubst]
x:154 [binder, in GMuAnnot.Prelude]
X:155 [binder, in GMuAnnot.InfrastructureSubst]
x:156 [binder, in GMuAnnot.Definitions]
x:160 [binder, in GMuAnnot.Preservation]
x:161 [binder, in GMuAnnot.Definitions]
X:161 [binder, in GMuAnnot.SubstMatch]
X:164 [binder, in GMuAnnot.SubstMatch]
x:165 [binder, in GMuAnnot.InfrastructureSubst]
x:165 [binder, in GMuAnnot.InfrastructureFV]
X:17 [binder, in GMuAnnot.InfrastructureSubst]
X:17 [binder, in GMuAnnot.InfrastructureOpen]
x:170 [binder, in GMuAnnot.Preservation]
x:172 [binder, in GMuAnnot.InfrastructureFV]
X:175 [binder, in GMuAnnot.SubstMatch]
X:178 [binder, in GMuAnnot.SubstMatch]
X:179 [binder, in GMuAnnot.InfrastructureSubst]
X:18 [binder, in GMuAnnot.Regularity]
x:185 [binder, in GMuAnnot.InfrastructureFV]
x:188 [binder, in GMuAnnot.Definitions]
X:188 [binder, in GMuAnnot.SubstMatch]
x:19 [binder, in GMuAnnot.Equations]
x:2 [binder, in GMuAnnot.InfrastructureFV]
x:2 [binder, in GMuAnnot.InfrastructureOpen]
x:2 [binder, in GMuAnnot.Prelude]
X:20 [binder, in GMuAnnot.Regularity]
x:202 [binder, in GMuAnnot.Preservation]
x:203 [binder, in GMuAnnot.Preservation]
X:203 [binder, in GMuAnnot.SubstMatch]
x:204 [binder, in GMuAnnot.Preservation]
x:205 [binder, in GMuAnnot.Preservation]
X:205 [binder, in GMuAnnot.SubstMatch]
x:206 [binder, in GMuAnnot.Preservation]
x:207 [binder, in GMuAnnot.Preservation]
x:21 [binder, in GMuAnnot.Equations]
X:21 [binder, in GMuAnnot.SubstMatch]
x:215 [binder, in GMuAnnot.Definitions]
x:220 [binder, in GMuAnnot.Preservation]
x:221 [binder, in GMuAnnot.Preservation]
X:225 [binder, in GMuAnnot.SubstMatch]
X:227 [binder, in GMuAnnot.SubstMatch]
x:23 [binder, in GMuAnnot.Equations]
X:232 [binder, in GMuAnnot.Definitions]
X:233 [binder, in GMuAnnot.Definitions]
X:24 [binder, in GMuAnnot.InfrastructureSubst]
x:25 [binder, in GMuAnnot.Equations]
X:25 [binder, in GMuAnnot.SubstMatch]
x:272 [binder, in GMuAnnot.Definitions]
x:273 [binder, in GMuAnnot.Definitions]
x:284 [binder, in GMuAnnot.Definitions]
X:29 [binder, in GMuAnnot.InfrastructureSubst]
x:3 [binder, in GMuAnnot.Prelude]
x:303 [binder, in GMuAnnot.Definitions]
X:32 [binder, in GMuAnnot.InfrastructureOpen]
X:36 [binder, in GMuAnnot.SubstMatch]
x:37 [binder, in GMuAnnot.InfrastructureFV]
x:4 [binder, in GMuAnnot.Prelude]
X:44 [binder, in GMuAnnot.InfrastructureSubst]
x:45 [binder, in GMuAnnot.Regularity]
X:45 [binder, in GMuAnnot.InfrastructureSubst]
x:46 [binder, in GMuAnnot.InfrastructureFV]
x:47 [binder, in GMuAnnot.InfrastructureOpen]
x:47 [binder, in GMuAnnot.Prelude]
X:48 [binder, in GMuAnnot.InfrastructureSubst]
x:49 [binder, in GMuAnnot.Preservation]
x:49 [binder, in GMuAnnot.Regularity2]
x:5 [binder, in GMuAnnot.Prelude]
x:51 [binder, in GMuAnnot.Regularity]
X:53 [binder, in GMuAnnot.InfrastructureSubst]
X:55 [binder, in GMuAnnot.InfrastructureSubst]
X:56 [binder, in GMuAnnot.Preservation]
x:56 [binder, in GMuAnnot.Regularity2]
X:56 [binder, in GMuAnnot.SubstMatch]
x:57 [binder, in GMuAnnot.Regularity]
X:59 [binder, in GMuAnnot.InfrastructureSubst]
X:6 [binder, in GMuAnnot.InfrastructureSubst]
x:6 [binder, in GMuAnnot.InfrastructureOpen]
x:6 [binder, in GMuAnnot.Prelude]
X:62 [binder, in GMuAnnot.Preservation]
x:62 [binder, in GMuAnnot.InfrastructureSubst]
X:65 [binder, in GMuAnnot.Regularity]
X:65 [binder, in GMuAnnot.InfrastructureFV]
X:67 [binder, in GMuAnnot.InfrastructureFV]
X:67 [binder, in GMuAnnot.SubstMatch]
X:68 [binder, in GMuAnnot.Preservation]
x:68 [binder, in GMuAnnot.Prelude]
x:69 [binder, in GMuAnnot.Regularity]
X:7 [binder, in GMuAnnot.InfrastructureSubstPrim]
x:7 [binder, in GMuAnnot.Prelude]
x:70 [binder, in GMuAnnot.InfrastructureSubst]
x:71 [binder, in GMuAnnot.InfrastructureFV]
x:71 [binder, in GMuAnnot.Prelude]
x:72 [binder, in GMuAnnot.InfrastructureSubst]
X:74 [binder, in GMuAnnot.Preservation]
x:74 [binder, in GMuAnnot.Regularity2]
X:76 [binder, in GMuAnnot.SubstMatch]
x:77 [binder, in GMuAnnot.InfrastructureFV]
x:78 [binder, in GMuAnnot.InfrastructureSubst]
x:8 [binder, in GMuAnnot.InfrastructureFV]
x:8 [binder, in GMuAnnot.Prelude]
x:81 [binder, in GMuAnnot.InfrastructureFV]
X:82 [binder, in GMuAnnot.Preservation]
x:84 [binder, in GMuAnnot.InfrastructureSubst]
x:84 [binder, in GMuAnnot.InfrastructureFV]
x:85 [binder, in GMuAnnot.Prelude]
x:86 [binder, in GMuAnnot.Prelude]
X:87 [binder, in GMuAnnot.SubstMatch]
X:88 [binder, in GMuAnnot.Preservation]
X:88 [binder, in GMuAnnot.InfrastructureFV]
X:88 [binder, in GMuAnnot.InfrastructureOpen]
x:89 [binder, in GMuAnnot.InfrastructureFV]
x:89 [binder, in GMuAnnot.Prelude]
x:9 [binder, in GMuAnnot.Regularity]
X:9 [binder, in GMuAnnot.InfrastructureOpen]
x:9 [binder, in GMuAnnot.Prelude]
X:90 [binder, in GMuAnnot.InfrastructureSubst]
X:91 [binder, in GMuAnnot.SubstMatch]
x:92 [binder, in GMuAnnot.InfrastructureOpen]
x:92 [binder, in GMuAnnot.Prelude]
X:94 [binder, in GMuAnnot.InfrastructureFV]
X:95 [binder, in GMuAnnot.SubstMatch]
X:97 [binder, in GMuAnnot.InfrastructureFV]
x:97 [binder, in GMuAnnot.Prelude]
x:98 [binder, in GMuAnnot.Preservation]
X:98 [binder, in GMuAnnot.SubstMatch]
Y
Y:102 [binder, in GMuAnnot.InfrastructureSubst]y:107 [binder, in GMuAnnot.InfrastructureSubst]
y:124 [binder, in GMuAnnot.Prelude]
Y:13 [binder, in GMuAnnot.SubstMatch]
Y:14 [binder, in GMuAnnot.InfrastructureSubst]
Y:144 [binder, in GMuAnnot.InfrastructureSubst]
Y:148 [binder, in GMuAnnot.InfrastructureSubst]
Y:15 [binder, in GMuAnnot.Preservation]
Y:23 [binder, in GMuAnnot.InfrastructureSubst]
Y:27 [binder, in GMuAnnot.InfrastructureSubst]
Y:30 [binder, in GMuAnnot.SubstMatch]
Y:50 [binder, in GMuAnnot.SubstMatch]
Y:56 [binder, in GMuAnnot.InfrastructureSubst]
Y:66 [binder, in GMuAnnot.InfrastructureFV]
Y:68 [binder, in GMuAnnot.Equations]
y:73 [binder, in GMuAnnot.InfrastructureSubst]
Y:81 [binder, in GMuAnnot.SubstMatch]
y:87 [binder, in GMuAnnot.Prelude]
y:90 [binder, in GMuAnnot.Prelude]
Z
z':62 [binder, in GMuAnnot.Prelude]Z:1 [binder, in GMuAnnot.InfrastructureSubst]
Z:106 [binder, in GMuAnnot.InfrastructureFV]
Z:110 [binder, in GMuAnnot.InfrastructureSubst]
Z:112 [binder, in GMuAnnot.InfrastructureFV]
Z:113 [binder, in GMuAnnot.InfrastructureSubst]
Z:116 [binder, in GMuAnnot.InfrastructureSubst]
Z:116 [binder, in GMuAnnot.InfrastructureFV]
z:117 [binder, in GMuAnnot.Prelude]
Z:120 [binder, in GMuAnnot.InfrastructureSubst]
Z:121 [binder, in GMuAnnot.InfrastructureFV]
Z:123 [binder, in GMuAnnot.Preservation]
Z:124 [binder, in GMuAnnot.InfrastructureSubst]
Z:127 [binder, in GMuAnnot.InfrastructureSubst]
Z:13 [binder, in GMuAnnot.InfrastructureFV]
Z:132 [binder, in GMuAnnot.InfrastructureSubst]
Z:133 [binder, in GMuAnnot.Preservation]
Z:134 [binder, in GMuAnnot.InfrastructureSubst]
Z:169 [binder, in GMuAnnot.Definitions]
Z:169 [binder, in GMuAnnot.InfrastructureSubst]
z:174 [binder, in GMuAnnot.Definitions]
Z:179 [binder, in GMuAnnot.InfrastructureFV]
Z:183 [binder, in GMuAnnot.InfrastructureFV]
Z:185 [binder, in GMuAnnot.InfrastructureSubst]
Z:187 [binder, in GMuAnnot.InfrastructureFV]
Z:188 [binder, in GMuAnnot.InfrastructureSubst]
Z:199 [binder, in GMuAnnot.SubstMatch]
Z:21 [binder, in GMuAnnot.InfrastructureFV]
Z:28 [binder, in GMuAnnot.InfrastructureFV]
Z:36 [binder, in GMuAnnot.InfrastructureFV]
Z:37 [binder, in GMuAnnot.Regularity2]
Z:43 [binder, in GMuAnnot.Regularity2]
z:45 [binder, in GMuAnnot.InfrastructureFV]
Z:59 [binder, in GMuAnnot.Regularity2]
z:61 [binder, in GMuAnnot.Prelude]
Z:68 [binder, in GMuAnnot.Regularity2]
Z:81 [binder, in GMuAnnot.InfrastructureSubst]
Z:83 [binder, in GMuAnnot.Regularity]
z:86 [binder, in GMuAnnot.InfrastructureSubst]
Z:92 [binder, in GMuAnnot.InfrastructureSubst]
Z:97 [binder, in GMuAnnot.InfrastructureSubst]
other
case_pattern:_ => _ (L2GMu) [notation, in GMuAnnot.Notations]_ <|| _ (L2GMu) [notation, in GMuAnnot.Notations]
_ <| _ (L2GMu) [notation, in GMuAnnot.Notations]
_ ==> _ (L2GMu) [notation, in GMuAnnot.Notations]
_ ** _ (L2GMu) [notation, in GMuAnnot.Notations]
case _ as _ of { _ | .. | _ } (L2GMu) [notation, in GMuAnnot.Notations]
enum _ {{ _ | .. | _ }} (L2GMu) [notation, in GMuAnnot.Notations]
fixs _ => _ (L2GMu) [notation, in GMuAnnot.Notations]
fst( _ ) (L2GMu) [notation, in GMuAnnot.Notations]
lets _ in _ tel (L2GMu) [notation, in GMuAnnot.Notations]
new _ [| _ , .. , _ |] ( _ ) (L2GMu) [notation, in GMuAnnot.Notations]
new _ [| |] ( _ ) (L2GMu) [notation, in GMuAnnot.Notations]
snd( _ ) (L2GMu) [notation, in GMuAnnot.Notations]
## _ (L2GMu) [notation, in GMuAnnot.Notations]
# _ (L2GMu) [notation, in GMuAnnot.Notations]
< _ , _ > (L2GMu) [notation, in GMuAnnot.Notations]
<.> (L2GMu) [notation, in GMuAnnot.Notations]
Λ => _ (L2GMu) [notation, in GMuAnnot.Notations]
γ( _ , .. , _ ) _ (L2GMu) [notation, in GMuAnnot.Notations]
γ() _ (L2GMu) [notation, in GMuAnnot.Notations]
λ _ => _ (L2GMu) [notation, in GMuAnnot.Notations]
∀ _ (L2GMu) [notation, in GMuAnnot.Notations]
_ --> _ [notation, in GMuAnnot.Definitions]
_ open_ee_varfix _ [notation, in GMuAnnot.Definitions]
_ open_ee_varlam _ [notation, in GMuAnnot.Definitions]
_ open_te_var _ [notation, in GMuAnnot.Definitions]
{ _ , _ , _ } ⊢( _ ) _ ∈ _ [notation, in GMuAnnot.Definitions]
Δ1:120 [binder, in GMuAnnot.Preservation]
Δ1:128 [binder, in GMuAnnot.SubstMatch]
Δ1:144 [binder, in GMuAnnot.SubstMatch]
Δ1:158 [binder, in GMuAnnot.SubstMatch]
Δ1:171 [binder, in GMuAnnot.SubstMatch]
Δ1:178 [binder, in GMuAnnot.Preservation]
Δ1:184 [binder, in GMuAnnot.SubstMatch]
Δ1:191 [binder, in GMuAnnot.SubstMatch]
Δ1:197 [binder, in GMuAnnot.SubstMatch]
Δ1:236 [binder, in GMuAnnot.SubstMatch]
Δ1:243 [binder, in GMuAnnot.SubstMatch]
Δ2:121 [binder, in GMuAnnot.Preservation]
Δ2:141 [binder, in GMuAnnot.Preservation]
Δ2:179 [binder, in GMuAnnot.Preservation]
Δ2:185 [binder, in GMuAnnot.SubstMatch]
Δ2:192 [binder, in GMuAnnot.SubstMatch]
Δ2:198 [binder, in GMuAnnot.SubstMatch]
Δ2:237 [binder, in GMuAnnot.SubstMatch]
Δ2:244 [binder, in GMuAnnot.SubstMatch]
Δ:101 [binder, in GMuAnnot.Regularity]
Δ:104 [binder, in GMuAnnot.Regularity]
Δ:104 [binder, in GMuAnnot.SubstMatch]
Δ:109 [binder, in GMuAnnot.SubstMatch]
Δ:11 [binder, in GMuAnnot.CanonicalForms]
Δ:114 [binder, in GMuAnnot.Regularity]
Δ:115 [binder, in GMuAnnot.SubstMatch]
Δ:118 [binder, in GMuAnnot.Regularity]
Δ:12 [binder, in GMuAnnot.Equations]
Δ:120 [binder, in GMuAnnot.SubstMatch]
Δ:122 [binder, in GMuAnnot.SubstMatch]
Δ:126 [binder, in GMuAnnot.InfrastructureFV]
Δ:128 [binder, in GMuAnnot.Regularity]
Δ:131 [binder, in GMuAnnot.Preservation]
Δ:134 [binder, in GMuAnnot.Regularity]
Δ:138 [binder, in GMuAnnot.InfrastructureFV]
Δ:140 [binder, in GMuAnnot.Preservation]
Δ:157 [binder, in GMuAnnot.Preservation]
Δ:16 [binder, in GMuAnnot.Equations]
Δ:168 [binder, in GMuAnnot.Preservation]
Δ:18 [binder, in GMuAnnot.Preservation]
Δ:182 [binder, in GMuAnnot.InfrastructureFV]
Δ:182 [binder, in GMuAnnot.SubstMatch]
Δ:183 [binder, in GMuAnnot.Definitions]
Δ:186 [binder, in GMuAnnot.InfrastructureFV]
Δ:187 [binder, in GMuAnnot.Definitions]
Δ:187 [binder, in GMuAnnot.Preservation]
Δ:193 [binder, in GMuAnnot.Definitions]
Δ:2 [binder, in GMuAnnot.CanonicalForms]
Δ:2 [binder, in GMuAnnot.Equations]
Δ:20 [binder, in GMuAnnot.CanonicalForms]
Δ:208 [binder, in GMuAnnot.SubstMatch]
Δ:209 [binder, in GMuAnnot.Definitions]
Δ:215 [binder, in GMuAnnot.SubstMatch]
Δ:217 [binder, in GMuAnnot.Definitions]
Δ:227 [binder, in GMuAnnot.Definitions]
Δ:235 [binder, in GMuAnnot.Definitions]
Δ:243 [binder, in GMuAnnot.Definitions]
Δ:252 [binder, in GMuAnnot.Definitions]
Δ:259 [binder, in GMuAnnot.Definitions]
Δ:267 [binder, in GMuAnnot.Definitions]
Δ:27 [binder, in GMuAnnot.CanonicalForms]
Δ:27 [binder, in GMuAnnot.Preservation]
Δ:276 [binder, in GMuAnnot.Definitions]
Δ:287 [binder, in GMuAnnot.Definitions]
Δ:306 [binder, in GMuAnnot.Definitions]
Δ:32 [binder, in GMuAnnot.Equations]
Δ:33 [binder, in GMuAnnot.CanonicalForms]
Δ:36 [binder, in GMuAnnot.Preservation]
Δ:36 [binder, in GMuAnnot.Regularity]
Δ:37 [binder, in GMuAnnot.Equations]
Δ:38 [binder, in GMuAnnot.CanonicalForms]
Δ:4 [binder, in GMuAnnot.Equations]
Δ:40 [binder, in GMuAnnot.Regularity]
Δ:41 [binder, in GMuAnnot.CanonicalForms]
Δ:43 [binder, in GMuAnnot.Regularity]
Δ:45 [binder, in GMuAnnot.Equations]
Δ:46 [binder, in GMuAnnot.Preservation]
Δ:47 [binder, in GMuAnnot.Regularity2]
Δ:49 [binder, in GMuAnnot.Regularity]
Δ:5 [binder, in GMuAnnot.Regularity]
Δ:52 [binder, in GMuAnnot.Equations]
Δ:53 [binder, in GMuAnnot.Regularity2]
Δ:55 [binder, in GMuAnnot.Regularity]
Δ:59 [binder, in GMuAnnot.Equations]
Δ:66 [binder, in GMuAnnot.Equations]
Δ:67 [binder, in GMuAnnot.Regularity]
Δ:7 [binder, in GMuAnnot.Equations]
Δ:71 [binder, in GMuAnnot.Regularity2]
Δ:72 [binder, in GMuAnnot.Equations]
Δ:73 [binder, in GMuAnnot.Regularity]
Δ:78 [binder, in GMuAnnot.Equations]
Δ:8 [binder, in GMuAnnot.Regularity]
Δ:84 [binder, in GMuAnnot.Equations]
Δ:87 [binder, in GMuAnnot.Regularity]
Δ:88 [binder, in GMuAnnot.Equations]
Δ:94 [binder, in GMuAnnot.SubstMatch]
Δ:95 [binder, in GMuAnnot.Preservation]
Θ1:15 [binder, in GMuAnnot.SubstMatch]
Θ1:54 [binder, in GMuAnnot.SubstMatch]
Θ1:63 [binder, in GMuAnnot.SubstMatch]
Θ1:72 [binder, in GMuAnnot.SubstMatch]
Θ2:16 [binder, in GMuAnnot.SubstMatch]
Θ2:55 [binder, in GMuAnnot.SubstMatch]
Θ2:64 [binder, in GMuAnnot.SubstMatch]
Θ2:73 [binder, in GMuAnnot.SubstMatch]
Θ:1 [binder, in GMuAnnot.InfrastructureSubstPrim]
Θ:13 [binder, in GMuAnnot.Equations]
Θ:14 [binder, in GMuAnnot.SubstMatch]
Θ:3 [binder, in GMuAnnot.InfrastructureSubstPrim]
Θ:3 [binder, in GMuAnnot.SubstMatch]
Θ:31 [binder, in GMuAnnot.Equations]
Θ:38 [binder, in GMuAnnot.Equations]
Θ:41 [binder, in GMuAnnot.Equations]
Θ:47 [binder, in GMuAnnot.SubstMatch]
Θ:5 [binder, in GMuAnnot.SubstMatch]
Θ:67 [binder, in GMuAnnot.Equations]
Σ:1 [binder, in GMuAnnot.CanonicalForms]
Σ:1 [binder, in GMuAnnot.Regularity]
Σ:1 [binder, in GMuAnnot.Regularity2]
Σ:1 [binder, in GMuAnnot.SubstMatch]
Σ:10 [binder, in GMuAnnot.CanonicalForms]
Σ:10 [binder, in GMuAnnot.Preservation]
Σ:10 [binder, in GMuAnnot.SubstMatch]
Σ:102 [binder, in GMuAnnot.SubstMatch]
Σ:105 [binder, in GMuAnnot.Regularity]
Σ:107 [binder, in GMuAnnot.SubstMatch]
Σ:11 [binder, in GMuAnnot.Equations]
Σ:112 [binder, in GMuAnnot.SubstMatch]
Σ:113 [binder, in GMuAnnot.Regularity]
Σ:117 [binder, in GMuAnnot.Regularity]
Σ:117 [binder, in GMuAnnot.SubstMatch]
Σ:119 [binder, in GMuAnnot.Preservation]
Σ:121 [binder, in GMuAnnot.SubstMatch]
Σ:127 [binder, in GMuAnnot.Regularity]
Σ:127 [binder, in GMuAnnot.SubstMatch]
Σ:13 [binder, in GMuAnnot.Regularity]
Σ:130 [binder, in GMuAnnot.Preservation]
Σ:133 [binder, in GMuAnnot.Regularity]
Σ:137 [binder, in GMuAnnot.InfrastructureFV]
Σ:139 [binder, in GMuAnnot.Preservation]
Σ:14 [binder, in GMuAnnot.Regularity2]
Σ:143 [binder, in GMuAnnot.SubstMatch]
Σ:156 [binder, in GMuAnnot.Preservation]
Σ:157 [binder, in GMuAnnot.SubstMatch]
Σ:167 [binder, in GMuAnnot.Preservation]
Σ:17 [binder, in GMuAnnot.Preservation]
Σ:170 [binder, in GMuAnnot.SubstMatch]
Σ:177 [binder, in GMuAnnot.Preservation]
Σ:18 [binder, in GMuAnnot.SubstMatch]
Σ:180 [binder, in GMuAnnot.SubstMatch]
Σ:182 [binder, in GMuAnnot.Definitions]
Σ:183 [binder, in GMuAnnot.SubstMatch]
Σ:185 [binder, in GMuAnnot.Definitions]
Σ:186 [binder, in GMuAnnot.Preservation]
Σ:19 [binder, in GMuAnnot.CanonicalForms]
Σ:19 [binder, in GMuAnnot.Regularity2]
Σ:190 [binder, in GMuAnnot.SubstMatch]
Σ:191 [binder, in GMuAnnot.Definitions]
Σ:196 [binder, in GMuAnnot.SubstMatch]
Σ:2 [binder, in GMuAnnot.Preservation]
Σ:207 [binder, in GMuAnnot.SubstMatch]
Σ:208 [binder, in GMuAnnot.Definitions]
Σ:214 [binder, in GMuAnnot.SubstMatch]
Σ:216 [binder, in GMuAnnot.Definitions]
Σ:22 [binder, in GMuAnnot.Regularity]
Σ:226 [binder, in GMuAnnot.Definitions]
Σ:229 [binder, in GMuAnnot.SubstMatch]
Σ:23 [binder, in GMuAnnot.SubstMatch]
Σ:234 [binder, in GMuAnnot.Definitions]
Σ:235 [binder, in GMuAnnot.SubstMatch]
Σ:242 [binder, in GMuAnnot.Definitions]
Σ:242 [binder, in GMuAnnot.SubstMatch]
Σ:251 [binder, in GMuAnnot.Definitions]
Σ:258 [binder, in GMuAnnot.Definitions]
Σ:26 [binder, in GMuAnnot.CanonicalForms]
Σ:26 [binder, in GMuAnnot.Preservation]
Σ:26 [binder, in GMuAnnot.Regularity2]
Σ:266 [binder, in GMuAnnot.Definitions]
Σ:27 [binder, in GMuAnnot.Regularity]
Σ:275 [binder, in GMuAnnot.Definitions]
Σ:286 [binder, in GMuAnnot.Definitions]
Σ:29 [binder, in GMuAnnot.Equations]
Σ:3 [binder, in GMuAnnot.Progress]
Σ:305 [binder, in GMuAnnot.Definitions]
Σ:32 [binder, in GMuAnnot.CanonicalForms]
Σ:34 [binder, in GMuAnnot.Regularity]
Σ:34 [binder, in GMuAnnot.Regularity2]
Σ:34 [binder, in GMuAnnot.SubstMatch]
Σ:35 [binder, in GMuAnnot.Preservation]
Σ:36 [binder, in GMuAnnot.Equations]
Σ:37 [binder, in GMuAnnot.CanonicalForms]
Σ:380 [binder, in GMuAnnot.Definitions]
Σ:385 [binder, in GMuAnnot.Definitions]
Σ:39 [binder, in GMuAnnot.Regularity]
Σ:4 [binder, in GMuAnnot.Regularity]
Σ:4 [binder, in GMuAnnot.SubstMatch]
Σ:40 [binder, in GMuAnnot.CanonicalForms]
Σ:40 [binder, in GMuAnnot.Regularity2]
Σ:40 [binder, in GMuAnnot.SubstMatch]
Σ:42 [binder, in GMuAnnot.Regularity]
Σ:44 [binder, in GMuAnnot.Equations]
Σ:45 [binder, in GMuAnnot.Preservation]
Σ:46 [binder, in GMuAnnot.Regularity2]
Σ:48 [binder, in GMuAnnot.Regularity]
Σ:5 [binder, in GMuAnnot.Regularity2]
Σ:50 [binder, in GMuAnnot.Equations]
Σ:51 [binder, in GMuAnnot.Equations]
Σ:52 [binder, in GMuAnnot.Regularity2]
Σ:54 [binder, in GMuAnnot.Regularity]
Σ:58 [binder, in GMuAnnot.Equations]
Σ:58 [binder, in GMuAnnot.SubstMatch]
Σ:61 [binder, in GMuAnnot.Regularity]
Σ:64 [binder, in GMuAnnot.Regularity2]
Σ:65 [binder, in GMuAnnot.Equations]
Σ:66 [binder, in GMuAnnot.Regularity]
Σ:7 [binder, in GMuAnnot.Regularity]
Σ:70 [binder, in GMuAnnot.Regularity2]
Σ:71 [binder, in GMuAnnot.Equations]
Σ:71 [binder, in GMuAnnot.SubstMatch]
Σ:72 [binder, in GMuAnnot.Regularity]
Σ:75 [binder, in GMuAnnot.Regularity]
Σ:77 [binder, in GMuAnnot.Equations]
Σ:78 [binder, in GMuAnnot.Regularity2]
Σ:78 [binder, in GMuAnnot.SubstMatch]
Σ:80 [binder, in GMuAnnot.Regularity]
Σ:83 [binder, in GMuAnnot.Equations]
Σ:84 [binder, in GMuAnnot.SubstMatch]
Σ:86 [binder, in GMuAnnot.Regularity]
Σ:87 [binder, in GMuAnnot.Equations]
Σ:9 [binder, in GMuAnnot.Regularity2]
Σ:90 [binder, in GMuAnnot.Regularity]
Σ:92 [binder, in GMuAnnot.SubstMatch]
Σ:94 [binder, in GMuAnnot.Preservation]
Σ:98 [binder, in GMuAnnot.Regularity]
ϵ:142 [binder, in GMuAnnot.InfrastructureFV]
ϵ:171 [binder, in GMuAnnot.Prelude]
ϵ:25 [binder, in GMuAnnot.Preservation]
ϵ:25 [binder, in GMuAnnot.Regularity]
ϵ:25 [binder, in GMuAnnot.Regularity2]
ϵ:33 [binder, in GMuAnnot.Regularity]
Notation Index
other
case_pattern:_ => _ (L2GMu) [in GMuAnnot.Notations]_ <|| _ (L2GMu) [in GMuAnnot.Notations]
_ <| _ (L2GMu) [in GMuAnnot.Notations]
_ ==> _ (L2GMu) [in GMuAnnot.Notations]
_ ** _ (L2GMu) [in GMuAnnot.Notations]
case _ as _ of { _ | .. | _ } (L2GMu) [in GMuAnnot.Notations]
enum _ {{ _ | .. | _ }} (L2GMu) [in GMuAnnot.Notations]
fixs _ => _ (L2GMu) [in GMuAnnot.Notations]
fst( _ ) (L2GMu) [in GMuAnnot.Notations]
lets _ in _ tel (L2GMu) [in GMuAnnot.Notations]
new _ [| _ , .. , _ |] ( _ ) (L2GMu) [in GMuAnnot.Notations]
new _ [| |] ( _ ) (L2GMu) [in GMuAnnot.Notations]
snd( _ ) (L2GMu) [in GMuAnnot.Notations]
## _ (L2GMu) [in GMuAnnot.Notations]
# _ (L2GMu) [in GMuAnnot.Notations]
< _ , _ > (L2GMu) [in GMuAnnot.Notations]
<.> (L2GMu) [in GMuAnnot.Notations]
Λ => _ (L2GMu) [in GMuAnnot.Notations]
γ( _ , .. , _ ) _ (L2GMu) [in GMuAnnot.Notations]
γ() _ (L2GMu) [in GMuAnnot.Notations]
λ _ => _ (L2GMu) [in GMuAnnot.Notations]
∀ _ (L2GMu) [in GMuAnnot.Notations]
_ --> _ [in GMuAnnot.Definitions]
_ open_ee_varfix _ [in GMuAnnot.Definitions]
_ open_ee_varlam _ [in GMuAnnot.Definitions]
_ open_te_var _ [in GMuAnnot.Definitions]
{ _ , _ , _ } ⊢( _ ) _ ∈ _ [in GMuAnnot.Definitions]
Binder Index
A
acc:149 [in GMuAnnot.Prelude]acc:151 [in GMuAnnot.Prelude]
acc:153 [in GMuAnnot.Prelude]
acc:155 [in GMuAnnot.Prelude]
acc:20 [in GMuAnnot.Equations]
acc:22 [in GMuAnnot.Equations]
acc:24 [in GMuAnnot.Equations]
acc:26 [in GMuAnnot.Equations]
Ah:132 [in GMuAnnot.Prelude]
Alphas:106 [in GMuAnnot.Regularity]
Alphas:155 [in GMuAnnot.Definitions]
Alphas:302 [in GMuAnnot.Definitions]
Alphas:75 [in GMuAnnot.Prelude]
args:103 [in GMuAnnot.Definitions]
args:99 [in GMuAnnot.Definitions]
As:119 [in GMuAnnot.InfrastructureFV]
As:128 [in GMuAnnot.InfrastructureOpen]
As:138 [in GMuAnnot.Preservation]
As:140 [in GMuAnnot.InfrastructureOpen]
As:153 [in GMuAnnot.InfrastructureFV]
As:158 [in GMuAnnot.InfrastructureSubst]
As:162 [in GMuAnnot.InfrastructureSubst]
As:162 [in GMuAnnot.InfrastructureFV]
As:169 [in GMuAnnot.InfrastructureFV]
As:172 [in GMuAnnot.InfrastructureSubst]
As:176 [in GMuAnnot.InfrastructureSubst]
As:181 [in GMuAnnot.InfrastructureFV]
As:197 [in GMuAnnot.Preservation]
As:209 [in GMuAnnot.SubstMatch]
As:27 [in GMuAnnot.Equations]
As:29 [in GMuAnnot.Preservation]
As:29 [in GMuAnnot.Regularity2]
As:30 [in GMuAnnot.Equations]
As:35 [in GMuAnnot.Equations]
As:35 [in GMuAnnot.Regularity]
As:69 [in GMuAnnot.InfrastructureFV]
As:96 [in GMuAnnot.InfrastructureOpen]
As:96 [in GMuAnnot.Prelude]
As:99 [in GMuAnnot.Regularity]
Ats:133 [in GMuAnnot.Prelude]
A:1 [in GMuAnnot.InfrastructureFV]
A:105 [in GMuAnnot.SubstMatch]
A:107 [in GMuAnnot.Prelude]
A:109 [in GMuAnnot.Regularity]
A:110 [in GMuAnnot.Regularity]
A:110 [in GMuAnnot.SubstMatch]
A:112 [in GMuAnnot.Prelude]
A:117 [in GMuAnnot.Preservation]
A:118 [in GMuAnnot.Preservation]
a:118 [in GMuAnnot.Prelude]
a:120 [in GMuAnnot.Prelude]
A:122 [in GMuAnnot.Prelude]
A:125 [in GMuAnnot.Regularity]
A:126 [in GMuAnnot.Regularity]
A:129 [in GMuAnnot.Prelude]
A:138 [in GMuAnnot.Prelude]
A:142 [in GMuAnnot.Prelude]
A:146 [in GMuAnnot.Prelude]
A:149 [in GMuAnnot.Preservation]
A:149 [in GMuAnnot.InfrastructureFV]
A:150 [in GMuAnnot.Preservation]
A:151 [in GMuAnnot.Preservation]
A:152 [in GMuAnnot.Preservation]
A:153 [in GMuAnnot.Preservation]
A:154 [in GMuAnnot.InfrastructureFV]
A:155 [in GMuAnnot.Preservation]
A:157 [in GMuAnnot.Definitions]
A:157 [in GMuAnnot.Prelude]
A:160 [in GMuAnnot.Prelude]
A:161 [in GMuAnnot.InfrastructureSubst]
a:165 [in GMuAnnot.Prelude]
A:167 [in GMuAnnot.InfrastructureSubst]
A:167 [in GMuAnnot.InfrastructureFV]
A:172 [in GMuAnnot.Prelude]
A:174 [in GMuAnnot.InfrastructureSubst]
A:176 [in GMuAnnot.Prelude]
A:177 [in GMuAnnot.InfrastructureFV]
A:178 [in GMuAnnot.InfrastructureSubst]
A:181 [in GMuAnnot.InfrastructureSubst]
A:183 [in GMuAnnot.Prelude]
A:20 [in GMuAnnot.InfrastructureFV]
A:200 [in GMuAnnot.Preservation]
A:208 [in GMuAnnot.Preservation]
A:209 [in GMuAnnot.Preservation]
A:233 [in GMuAnnot.SubstMatch]
A:25 [in GMuAnnot.InfrastructureSubstPrim]
A:28 [in GMuAnnot.Equations]
A:30 [in GMuAnnot.InfrastructureSubst]
A:304 [in GMuAnnot.Definitions]
A:31 [in GMuAnnot.Regularity2]
A:32 [in GMuAnnot.Regularity2]
A:33 [in GMuAnnot.Preservation]
A:33 [in GMuAnnot.Regularity2]
A:34 [in GMuAnnot.Equations]
A:34 [in GMuAnnot.Preservation]
A:36 [in GMuAnnot.InfrastructureSubst]
A:38 [in GMuAnnot.Regularity]
A:39 [in GMuAnnot.Equations]
A:4 [in GMuAnnot.InfrastructureSubstPrim]
A:42 [in GMuAnnot.Equations]
A:42 [in GMuAnnot.InfrastructureFV]
A:43 [in GMuAnnot.Preservation]
A:44 [in GMuAnnot.Preservation]
A:44 [in GMuAnnot.Prelude]
A:46 [in GMuAnnot.Equations]
A:48 [in GMuAnnot.Prelude]
A:52 [in GMuAnnot.SubstMatch]
a:53 [in GMuAnnot.Prelude]
A:55 [in GMuAnnot.Prelude]
a:63 [in GMuAnnot.Prelude]
a:65 [in GMuAnnot.Prelude]
A:67 [in GMuAnnot.Prelude]
A:69 [in GMuAnnot.Equations]
A:69 [in GMuAnnot.SubstMatch]
A:70 [in GMuAnnot.Definitions]
A:70 [in GMuAnnot.Prelude]
A:76 [in GMuAnnot.Prelude]
A:77 [in GMuAnnot.Prelude]
a:78 [in GMuAnnot.Prelude]
A:79 [in GMuAnnot.Prelude]
A:80 [in GMuAnnot.Preservation]
A:81 [in GMuAnnot.Preservation]
A:93 [in GMuAnnot.Prelude]
A:98 [in GMuAnnot.Prelude]
A:99 [in GMuAnnot.Prelude]
A:99 [in GMuAnnot.SubstMatch]
B
base:10 [in GMuAnnot.InfrastructureFV]base:15 [in GMuAnnot.InfrastructureFV]
base:25 [in GMuAnnot.InfrastructureFV]
base:31 [in GMuAnnot.InfrastructureFV]
base:39 [in GMuAnnot.InfrastructureFV]
base:5 [in GMuAnnot.InfrastructureFV]
B:100 [in GMuAnnot.Prelude]
B:100 [in GMuAnnot.SubstMatch]
B:113 [in GMuAnnot.Prelude]
b:119 [in GMuAnnot.Prelude]
b:121 [in GMuAnnot.Prelude]
B:139 [in GMuAnnot.Prelude]
B:143 [in GMuAnnot.Prelude]
B:147 [in GMuAnnot.Prelude]
B:158 [in GMuAnnot.Prelude]
B:161 [in GMuAnnot.Prelude]
B:163 [in GMuAnnot.InfrastructureFV]
b:166 [in GMuAnnot.Prelude]
B:170 [in GMuAnnot.InfrastructureFV]
B:177 [in GMuAnnot.Prelude]
B:40 [in GMuAnnot.Equations]
B:43 [in GMuAnnot.Equations]
B:43 [in GMuAnnot.InfrastructureFV]
B:47 [in GMuAnnot.Equations]
B:49 [in GMuAnnot.Prelude]
B:56 [in GMuAnnot.Prelude]
B:58 [in GMuAnnot.Prelude]
b:64 [in GMuAnnot.Prelude]
b:66 [in GMuAnnot.Prelude]
B:80 [in GMuAnnot.Prelude]
B:94 [in GMuAnnot.Prelude]
C
CargType:202 [in GMuAnnot.Definitions]CargType:96 [in GMuAnnot.Regularity]
Carity:201 [in GMuAnnot.Definitions]
Carity:340 [in GMuAnnot.Definitions]
Carity:95 [in GMuAnnot.Regularity]
Ce:341 [in GMuAnnot.Definitions]
cid:337 [in GMuAnnot.Definitions]
clArity:5 [in GMuAnnot.Definitions]
Clauses:186 [in GMuAnnot.Prelude]
clauses:45 [in GMuAnnot.Definitions]
clauses:56 [in GMuAnnot.Definitions]
clause:299 [in GMuAnnot.Definitions]
clause:301 [in GMuAnnot.Definitions]
clause:7 [in GMuAnnot.Progress]
clause:9 [in GMuAnnot.Progress]
clA:189 [in GMuAnnot.Prelude]
clT:190 [in GMuAnnot.Prelude]
cl:154 [in GMuAnnot.Definitions]
cl:17 [in GMuAnnot.InfrastructureFV]
cl:18 [in GMuAnnot.InfrastructureFV]
cl:188 [in GMuAnnot.Prelude]
cl:19 [in GMuAnnot.InfrastructureFV]
cl:29 [in GMuAnnot.InfrastructureFV]
cl:33 [in GMuAnnot.InfrastructureFV]
cl:34 [in GMuAnnot.InfrastructureFV]
cl:35 [in GMuAnnot.InfrastructureFV]
cl:86 [in GMuAnnot.InfrastructureOpen]
CretTypes:203 [in GMuAnnot.Definitions]
CretTypes:97 [in GMuAnnot.Regularity]
cs:72 [in GMuAnnot.Definitions]
cs:75 [in GMuAnnot.Definitions]
Ctors:200 [in GMuAnnot.Definitions]
Ctors:93 [in GMuAnnot.Regularity]
Ctor:14 [in GMuAnnot.CanonicalForms]
Ctor:197 [in GMuAnnot.Definitions]
Ctor:348 [in GMuAnnot.Definitions]
Ctor:6 [in GMuAnnot.CanonicalForms]
Ctor:94 [in GMuAnnot.Regularity]
C:101 [in GMuAnnot.Prelude]
c:101 [in GMuAnnot.SubstMatch]
c:109 [in GMuAnnot.Definitions]
C:133 [in GMuAnnot.InfrastructureFV]
C:140 [in GMuAnnot.Prelude]
C:159 [in GMuAnnot.Prelude]
C:46 [in GMuAnnot.CanonicalForms]
C:48 [in GMuAnnot.Equations]
c:49 [in GMuAnnot.Definitions]
c:57 [in GMuAnnot.Definitions]
C:57 [in GMuAnnot.Prelude]
c:60 [in GMuAnnot.Definitions]
c:61 [in GMuAnnot.Definitions]
c:63 [in GMuAnnot.Definitions]
c:7 [in GMuAnnot.Definitions]
c:73 [in GMuAnnot.Definitions]
c:76 [in GMuAnnot.Definitions]
C:81 [in GMuAnnot.Prelude]
c:86 [in GMuAnnot.Definitions]
c:9 [in GMuAnnot.Definitions]
c:93 [in GMuAnnot.Definitions]
C:95 [in GMuAnnot.Prelude]
D
Defs:185 [in GMuAnnot.Prelude]Defs:296 [in GMuAnnot.Definitions]
def:187 [in GMuAnnot.Prelude]
def:298 [in GMuAnnot.Definitions]
def:300 [in GMuAnnot.Definitions]
def:6 [in GMuAnnot.Progress]
def:8 [in GMuAnnot.Progress]
Deqs:140 [in GMuAnnot.InfrastructureFV]
Deqs:20 [in GMuAnnot.Preservation]
Deqs:22 [in GMuAnnot.Regularity2]
Deqs:29 [in GMuAnnot.Regularity]
D':89 [in GMuAnnot.SubstMatch]
D1:10 [in GMuAnnot.Regularity2]
D1:11 [in GMuAnnot.Preservation]
D1:11 [in GMuAnnot.SubstMatch]
D1:14 [in GMuAnnot.Regularity]
D1:15 [in GMuAnnot.Regularity2]
D1:151 [in GMuAnnot.InfrastructureFV]
D1:173 [in GMuAnnot.InfrastructureFV]
D1:20 [in GMuAnnot.Regularity2]
D1:23 [in GMuAnnot.Regularity]
D1:230 [in GMuAnnot.SubstMatch]
D1:24 [in GMuAnnot.SubstMatch]
D1:27 [in GMuAnnot.Regularity2]
D1:28 [in GMuAnnot.Regularity]
D1:3 [in GMuAnnot.Preservation]
D1:35 [in GMuAnnot.Regularity2]
D1:35 [in GMuAnnot.SubstMatch]
D1:41 [in GMuAnnot.Regularity2]
D1:41 [in GMuAnnot.SubstMatch]
D1:59 [in GMuAnnot.SubstMatch]
D1:6 [in GMuAnnot.Regularity2]
D1:6 [in GMuAnnot.SubstMatch]
D1:62 [in GMuAnnot.Regularity]
D1:65 [in GMuAnnot.Regularity2]
D1:74 [in GMuAnnot.SubstMatch]
D1:76 [in GMuAnnot.Regularity]
D1:79 [in GMuAnnot.Regularity2]
D1:79 [in GMuAnnot.SubstMatch]
D1:81 [in GMuAnnot.Regularity]
D1:92 [in GMuAnnot.InfrastructureFV]
D1:95 [in GMuAnnot.InfrastructureFV]
D2:11 [in GMuAnnot.Regularity2]
D2:116 [in GMuAnnot.SubstMatch]
D2:12 [in GMuAnnot.Preservation]
D2:12 [in GMuAnnot.SubstMatch]
D2:15 [in GMuAnnot.Regularity]
D2:152 [in GMuAnnot.InfrastructureFV]
D2:16 [in GMuAnnot.Regularity2]
D2:174 [in GMuAnnot.InfrastructureFV]
D2:21 [in GMuAnnot.Regularity2]
D2:232 [in GMuAnnot.SubstMatch]
D2:24 [in GMuAnnot.Regularity]
D2:26 [in GMuAnnot.SubstMatch]
D2:28 [in GMuAnnot.Regularity2]
D2:30 [in GMuAnnot.Regularity]
D2:36 [in GMuAnnot.Regularity2]
D2:37 [in GMuAnnot.SubstMatch]
D2:4 [in GMuAnnot.Preservation]
D2:42 [in GMuAnnot.Regularity2]
D2:42 [in GMuAnnot.SubstMatch]
D2:60 [in GMuAnnot.SubstMatch]
D2:63 [in GMuAnnot.Regularity]
D2:66 [in GMuAnnot.Regularity2]
D2:7 [in GMuAnnot.Regularity2]
D2:7 [in GMuAnnot.SubstMatch]
D2:75 [in GMuAnnot.SubstMatch]
D2:77 [in GMuAnnot.Regularity]
D2:80 [in GMuAnnot.Regularity2]
D2:80 [in GMuAnnot.SubstMatch]
D2:82 [in GMuAnnot.Regularity]
D2:93 [in GMuAnnot.InfrastructureFV]
D2:96 [in GMuAnnot.InfrastructureFV]
D3:32 [in GMuAnnot.SubstMatch]
D3:78 [in GMuAnnot.Regularity]
D4:33 [in GMuAnnot.SubstMatch]
D:167 [in GMuAnnot.Prelude]
d:181 [in GMuAnnot.Prelude]
D:19 [in GMuAnnot.SubstMatch]
D:2 [in GMuAnnot.Regularity2]
D:2 [in GMuAnnot.SubstMatch]
D:224 [in GMuAnnot.SubstMatch]
D:49 [in GMuAnnot.Equations]
D:85 [in GMuAnnot.SubstMatch]
D:90 [in GMuAnnot.SubstMatch]
E
eq:141 [in GMuAnnot.InfrastructureFV]eq:170 [in GMuAnnot.Prelude]
eq:18 [in GMuAnnot.Regularity2]
eq:24 [in GMuAnnot.Preservation]
eq:24 [in GMuAnnot.Regularity2]
eq:32 [in GMuAnnot.Regularity]
eq:7 [in GMuAnnot.Preservation]
eq:82 [in GMuAnnot.Regularity2]
e':27 [in GMuAnnot.InfrastructureFV]
e':317 [in GMuAnnot.Definitions]
e':320 [in GMuAnnot.Definitions]
e':323 [in GMuAnnot.Definitions]
e':334 [in GMuAnnot.Definitions]
e':342 [in GMuAnnot.Definitions]
e':350 [in GMuAnnot.Definitions]
e':358 [in GMuAnnot.Definitions]
e':360 [in GMuAnnot.Definitions]
e':383 [in GMuAnnot.Definitions]
e':388 [in GMuAnnot.Definitions]
E0:106 [in GMuAnnot.Preservation]
E0:112 [in GMuAnnot.Preservation]
E0:57 [in GMuAnnot.Preservation]
E0:63 [in GMuAnnot.Preservation]
E0:69 [in GMuAnnot.Preservation]
E0:75 [in GMuAnnot.Preservation]
E0:83 [in GMuAnnot.Preservation]
E0:89 [in GMuAnnot.Preservation]
e1':345 [in GMuAnnot.Definitions]
e1':355 [in GMuAnnot.Definitions]
e1':363 [in GMuAnnot.Definitions]
e1':373 [in GMuAnnot.Definitions]
e1':377 [in GMuAnnot.Definitions]
e1:115 [in GMuAnnot.InfrastructureSubst]
e1:119 [in GMuAnnot.InfrastructureSubst]
e1:120 [in GMuAnnot.Definitions]
e1:122 [in GMuAnnot.Definitions]
e1:126 [in GMuAnnot.Definitions]
e1:127 [in GMuAnnot.Definitions]
e1:130 [in GMuAnnot.Definitions]
e1:132 [in GMuAnnot.Definitions]
e1:135 [in GMuAnnot.Definitions]
e1:146 [in GMuAnnot.Definitions]
e1:15 [in GMuAnnot.CanonicalForms]
e1:150 [in GMuAnnot.Definitions]
e1:159 [in GMuAnnot.Definitions]
e1:160 [in GMuAnnot.Definitions]
e1:162 [in GMuAnnot.Definitions]
e1:168 [in GMuAnnot.Definitions]
e1:184 [in GMuAnnot.InfrastructureSubst]
e1:187 [in GMuAnnot.InfrastructureSubst]
e1:198 [in GMuAnnot.Definitions]
e1:212 [in GMuAnnot.Definitions]
e1:221 [in GMuAnnot.Definitions]
e1:229 [in GMuAnnot.Definitions]
e1:237 [in GMuAnnot.Definitions]
e1:247 [in GMuAnnot.Definitions]
e1:256 [in GMuAnnot.Definitions]
e1:263 [in GMuAnnot.Definitions]
e1:280 [in GMuAnnot.Definitions]
e1:315 [in GMuAnnot.Definitions]
e1:318 [in GMuAnnot.Definitions]
e1:335 [in GMuAnnot.Definitions]
e1:344 [in GMuAnnot.Definitions]
e1:354 [in GMuAnnot.Definitions]
e1:361 [in GMuAnnot.Definitions]
e1:371 [in GMuAnnot.Definitions]
e1:374 [in GMuAnnot.Definitions]
e1:55 [in GMuAnnot.InfrastructureOpen]
e1:63 [in GMuAnnot.InfrastructureOpen]
e1:7 [in GMuAnnot.CanonicalForms]
e1:74 [in GMuAnnot.InfrastructureOpen]
e2':353 [in GMuAnnot.Definitions]
e2':368 [in GMuAnnot.Definitions]
e2:117 [in GMuAnnot.InfrastructureSubst]
e2:121 [in GMuAnnot.InfrastructureSubst]
e2:123 [in GMuAnnot.Definitions]
e2:133 [in GMuAnnot.Definitions]
e2:147 [in GMuAnnot.Definitions]
e2:163 [in GMuAnnot.Definitions]
e2:186 [in GMuAnnot.InfrastructureSubst]
e2:189 [in GMuAnnot.InfrastructureSubst]
e2:222 [in GMuAnnot.Definitions]
e2:248 [in GMuAnnot.Definitions]
e2:281 [in GMuAnnot.Definitions]
e2:322 [in GMuAnnot.Definitions]
e2:346 [in GMuAnnot.Definitions]
e2:352 [in GMuAnnot.Definitions]
e2:362 [in GMuAnnot.Definitions]
e2:367 [in GMuAnnot.Definitions]
e2:372 [in GMuAnnot.Definitions]
e2:56 [in GMuAnnot.InfrastructureOpen]
e2:64 [in GMuAnnot.InfrastructureOpen]
e2:75 [in GMuAnnot.InfrastructureOpen]
e:1 [in GMuAnnot.InfrastructureOpen]
e:1 [in GMuAnnot.Prelude]
e:100 [in GMuAnnot.Definitions]
e:100 [in GMuAnnot.InfrastructureSubst]
e:100 [in GMuAnnot.InfrastructureOpen]
e:101 [in GMuAnnot.Preservation]
E:102 [in GMuAnnot.Prelude]
e:104 [in GMuAnnot.Definitions]
e:105 [in GMuAnnot.Definitions]
e:105 [in GMuAnnot.InfrastructureSubst]
e:105 [in GMuAnnot.InfrastructureOpen]
e:109 [in GMuAnnot.InfrastructureSubst]
E:111 [in GMuAnnot.Prelude]
e:112 [in GMuAnnot.InfrastructureSubst]
e:115 [in GMuAnnot.InfrastructureOpen]
E:118 [in GMuAnnot.InfrastructureFV]
e:118 [in GMuAnnot.InfrastructureOpen]
E:119 [in GMuAnnot.Regularity]
E:12 [in GMuAnnot.CanonicalForms]
E:12 [in GMuAnnot.Regularity]
E:12 [in GMuAnnot.Regularity2]
e:120 [in GMuAnnot.Regularity]
E:122 [in GMuAnnot.Preservation]
E:122 [in GMuAnnot.InfrastructureFV]
e:123 [in GMuAnnot.InfrastructureOpen]
e:124 [in GMuAnnot.Preservation]
E:129 [in GMuAnnot.Regularity]
E:13 [in GMuAnnot.Preservation]
e:130 [in GMuAnnot.Regularity]
e:131 [in GMuAnnot.InfrastructureOpen]
E:132 [in GMuAnnot.Preservation]
E:132 [in GMuAnnot.InfrastructureFV]
e:133 [in GMuAnnot.InfrastructureOpen]
e:134 [in GMuAnnot.Preservation]
E:135 [in GMuAnnot.Regularity]
e:137 [in GMuAnnot.Regularity]
e:139 [in GMuAnnot.InfrastructureSubst]
E:142 [in GMuAnnot.Preservation]
e:142 [in GMuAnnot.InfrastructureSubst]
e:144 [in GMuAnnot.Preservation]
e:147 [in GMuAnnot.InfrastructureSubst]
e:152 [in GMuAnnot.InfrastructureSubst]
E:158 [in GMuAnnot.Preservation]
e:16 [in GMuAnnot.Prelude]
e:164 [in GMuAnnot.Preservation]
e:164 [in GMuAnnot.InfrastructureSubst]
E:168 [in GMuAnnot.InfrastructureSubst]
E:169 [in GMuAnnot.Preservation]
e:17 [in GMuAnnot.Definitions]
E:17 [in GMuAnnot.Regularity2]
e:17 [in GMuAnnot.Prelude]
e:171 [in GMuAnnot.Definitions]
e:174 [in GMuAnnot.Preservation]
E:175 [in GMuAnnot.InfrastructureSubst]
e:177 [in GMuAnnot.Definitions]
E:180 [in GMuAnnot.Preservation]
e:181 [in GMuAnnot.Preservation]
e:182 [in GMuAnnot.Prelude]
E:184 [in GMuAnnot.Definitions]
E:186 [in GMuAnnot.Definitions]
E:188 [in GMuAnnot.Preservation]
e:189 [in GMuAnnot.Preservation]
E:19 [in GMuAnnot.Preservation]
e:19 [in GMuAnnot.Prelude]
E:192 [in GMuAnnot.Definitions]
E:2 [in GMuAnnot.Regularity]
e:21 [in GMuAnnot.CanonicalForms]
e:21 [in GMuAnnot.Prelude]
E:210 [in GMuAnnot.Definitions]
E:218 [in GMuAnnot.Definitions]
e:22 [in GMuAnnot.InfrastructureFV]
E:223 [in GMuAnnot.SubstMatch]
E:228 [in GMuAnnot.Definitions]
E:23 [in GMuAnnot.Regularity2]
e:23 [in GMuAnnot.Prelude]
E:236 [in GMuAnnot.Definitions]
E:244 [in GMuAnnot.Definitions]
E:253 [in GMuAnnot.Definitions]
e:26 [in GMuAnnot.Prelude]
E:260 [in GMuAnnot.Definitions]
E:268 [in GMuAnnot.Definitions]
e:27 [in GMuAnnot.Definitions]
e:27 [in GMuAnnot.Prelude]
E:277 [in GMuAnnot.Definitions]
e:28 [in GMuAnnot.CanonicalForms]
E:28 [in GMuAnnot.Preservation]
e:28 [in GMuAnnot.Prelude]
E:288 [in GMuAnnot.Definitions]
e:289 [in GMuAnnot.Definitions]
e:29 [in GMuAnnot.Definitions]
E:3 [in GMuAnnot.CanonicalForms]
E:3 [in GMuAnnot.Regularity2]
E:30 [in GMuAnnot.Regularity2]
E:307 [in GMuAnnot.Definitions]
e:31 [in GMuAnnot.Prelude]
e:310 [in GMuAnnot.Definitions]
e:32 [in GMuAnnot.Definitions]
e:32 [in GMuAnnot.Prelude]
e:34 [in GMuAnnot.CanonicalForms]
e:34 [in GMuAnnot.Prelude]
e:349 [in GMuAnnot.Definitions]
e:357 [in GMuAnnot.Definitions]
e:359 [in GMuAnnot.Definitions]
e:36 [in GMuAnnot.Prelude]
e:37 [in GMuAnnot.Definitions]
E:37 [in GMuAnnot.Preservation]
e:38 [in GMuAnnot.Prelude]
e:381 [in GMuAnnot.Definitions]
e:386 [in GMuAnnot.Definitions]
e:39 [in GMuAnnot.Definitions]
e:39 [in GMuAnnot.CanonicalForms]
e:40 [in GMuAnnot.Preservation]
E:41 [in GMuAnnot.Regularity]
e:42 [in GMuAnnot.Definitions]
e:42 [in GMuAnnot.CanonicalForms]
E:44 [in GMuAnnot.Regularity]
e:47 [in GMuAnnot.Definitions]
E:47 [in GMuAnnot.Preservation]
e:48 [in GMuAnnot.InfrastructureFV]
E:48 [in GMuAnnot.Regularity2]
E:5 [in GMuAnnot.Preservation]
e:5 [in GMuAnnot.InfrastructureOpen]
E:50 [in GMuAnnot.Regularity]
e:50 [in GMuAnnot.InfrastructureSubst]
e:50 [in GMuAnnot.InfrastructureFV]
e:51 [in GMuAnnot.InfrastructureSubst]
e:51 [in GMuAnnot.InfrastructureOpen]
e:52 [in GMuAnnot.Preservation]
E:53 [in GMuAnnot.Equations]
e:53 [in GMuAnnot.InfrastructureOpen]
e:54 [in GMuAnnot.Equations]
E:54 [in GMuAnnot.Regularity2]
E:56 [in GMuAnnot.Regularity]
e:58 [in GMuAnnot.InfrastructureSubst]
e:6 [in GMuAnnot.Definitions]
E:6 [in GMuAnnot.Regularity]
E:60 [in GMuAnnot.Equations]
e:60 [in GMuAnnot.InfrastructureOpen]
e:61 [in GMuAnnot.Equations]
e:61 [in GMuAnnot.InfrastructureSubst]
E:64 [in GMuAnnot.Regularity]
e:65 [in GMuAnnot.InfrastructureSubst]
e:66 [in GMuAnnot.InfrastructureOpen]
E:67 [in GMuAnnot.Regularity2]
E:68 [in GMuAnnot.Regularity]
e:68 [in GMuAnnot.InfrastructureOpen]
e:7 [in GMuAnnot.InfrastructureFV]
e:71 [in GMuAnnot.InfrastructureOpen]
E:72 [in GMuAnnot.Regularity2]
e:75 [in GMuAnnot.InfrastructureFV]
e:76 [in GMuAnnot.InfrastructureSubst]
e:78 [in GMuAnnot.Definitions]
e:79 [in GMuAnnot.InfrastructureOpen]
E:8 [in GMuAnnot.Regularity2]
e:80 [in GMuAnnot.InfrastructureSubst]
e:80 [in GMuAnnot.InfrastructureFV]
E:81 [in GMuAnnot.Regularity2]
e:82 [in GMuAnnot.InfrastructureOpen]
E:83 [in GMuAnnot.InfrastructureFV]
e:85 [in GMuAnnot.InfrastructureSubst]
E:87 [in GMuAnnot.InfrastructureFV]
e:87 [in GMuAnnot.InfrastructureOpen]
e:89 [in GMuAnnot.InfrastructureSubst]
e:90 [in GMuAnnot.Definitions]
e:91 [in GMuAnnot.InfrastructureOpen]
E:96 [in GMuAnnot.Preservation]
e:99 [in GMuAnnot.InfrastructureOpen]
F
fv:100 [in GMuAnnot.InfrastructureFV]fv:108 [in GMuAnnot.Definitions]
fv:108 [in GMuAnnot.InfrastructureFV]
fv:11 [in GMuAnnot.InfrastructureFV]
fv:110 [in GMuAnnot.Definitions]
fv:135 [in GMuAnnot.InfrastructureFV]
fv:16 [in GMuAnnot.InfrastructureFV]
fv:164 [in GMuAnnot.InfrastructureFV]
fv:171 [in GMuAnnot.InfrastructureFV]
fv:26 [in GMuAnnot.InfrastructureFV]
fv:32 [in GMuAnnot.InfrastructureFV]
fv:40 [in GMuAnnot.InfrastructureFV]
fv:49 [in GMuAnnot.InfrastructureFV]
fv:6 [in GMuAnnot.InfrastructureFV]
F0:107 [in GMuAnnot.Preservation]
F0:113 [in GMuAnnot.Preservation]
F0:19 [in GMuAnnot.Regularity]
F0:21 [in GMuAnnot.Regularity]
F0:58 [in GMuAnnot.Preservation]
F0:64 [in GMuAnnot.Preservation]
F0:70 [in GMuAnnot.Preservation]
F0:76 [in GMuAnnot.Preservation]
F0:84 [in GMuAnnot.Preservation]
F0:90 [in GMuAnnot.Preservation]
F1:95 [in GMuAnnot.Equations]
F2:96 [in GMuAnnot.Equations]
f:103 [in GMuAnnot.Prelude]
f:115 [in GMuAnnot.Prelude]
f:128 [in GMuAnnot.Prelude]
F:136 [in GMuAnnot.Prelude]
F:143 [in GMuAnnot.Preservation]
F:159 [in GMuAnnot.Preservation]
f:162 [in GMuAnnot.Prelude]
F:178 [in GMuAnnot.Prelude]
F:184 [in GMuAnnot.Prelude]
F:38 [in GMuAnnot.Preservation]
F:4 [in GMuAnnot.Regularity2]
f:45 [in GMuAnnot.Prelude]
F:48 [in GMuAnnot.Preservation]
f:50 [in GMuAnnot.Prelude]
F:55 [in GMuAnnot.Regularity2]
F:60 [in GMuAnnot.Regularity]
f:71 [in GMuAnnot.Definitions]
F:73 [in GMuAnnot.Regularity2]
f:74 [in GMuAnnot.Definitions]
f:82 [in GMuAnnot.Prelude]
F:94 [in GMuAnnot.Equations]
F:97 [in GMuAnnot.Preservation]
G
GADTC:19 [in GMuAnnot.Definitions]GTs:136 [in GMuAnnot.InfrastructureOpen]
g:104 [in GMuAnnot.Prelude]
g:116 [in GMuAnnot.Prelude]
G:151 [in GMuAnnot.Definitions]
G:336 [in GMuAnnot.Definitions]
G:375 [in GMuAnnot.Definitions]
G:39 [in GMuAnnot.Preservation]
G:46 [in GMuAnnot.Definitions]
g:51 [in GMuAnnot.Prelude]
G:81 [in GMuAnnot.InfrastructureOpen]
g:83 [in GMuAnnot.Prelude]
H
head_proof:62 [in GMuAnnot.Definitions]h:105 [in GMuAnnot.Prelude]
I
i:122 [in GMuAnnot.InfrastructureOpen]i:127 [in GMuAnnot.InfrastructureOpen]
i:45 [in GMuAnnot.InfrastructureOpen]
J
j:119 [in GMuAnnot.InfrastructureOpen]j:124 [in GMuAnnot.InfrastructureOpen]
J:15 [in GMuAnnot.InfrastructureOpen]
K
k:108 [in GMuAnnot.InfrastructureSubst]k:108 [in GMuAnnot.InfrastructureOpen]
k:111 [in GMuAnnot.InfrastructureOpen]
k:114 [in GMuAnnot.InfrastructureOpen]
k:117 [in GMuAnnot.InfrastructureOpen]
k:118 [in GMuAnnot.InfrastructureSubst]
k:12 [in GMuAnnot.Prelude]
k:122 [in GMuAnnot.InfrastructureSubst]
k:129 [in GMuAnnot.InfrastructureOpen]
k:134 [in GMuAnnot.InfrastructureOpen]
k:14 [in GMuAnnot.Definitions]
k:16 [in GMuAnnot.InfrastructureOpen]
k:175 [in GMuAnnot.Definitions]
k:18 [in GMuAnnot.InfrastructureOpen]
k:19 [in GMuAnnot.InfrastructureOpen]
k:22 [in GMuAnnot.InfrastructureOpen]
k:25 [in GMuAnnot.InfrastructureOpen]
k:27 [in GMuAnnot.InfrastructureOpen]
k:30 [in GMuAnnot.InfrastructureOpen]
k:33 [in GMuAnnot.InfrastructureOpen]
k:39 [in GMuAnnot.InfrastructureOpen]
k:42 [in GMuAnnot.InfrastructureOpen]
k:46 [in GMuAnnot.InfrastructureOpen]
k:49 [in GMuAnnot.InfrastructureOpen]
k:50 [in GMuAnnot.InfrastructureOpen]
k:52 [in GMuAnnot.InfrastructureOpen]
k:53 [in GMuAnnot.InfrastructureFV]
k:54 [in GMuAnnot.InfrastructureOpen]
k:56 [in GMuAnnot.InfrastructureFV]
k:59 [in GMuAnnot.InfrastructureFV]
k:59 [in GMuAnnot.InfrastructureOpen]
k:62 [in GMuAnnot.InfrastructureFV]
k:62 [in GMuAnnot.InfrastructureOpen]
k:63 [in GMuAnnot.InfrastructureSubst]
k:65 [in GMuAnnot.InfrastructureOpen]
k:67 [in GMuAnnot.InfrastructureOpen]
k:69 [in GMuAnnot.InfrastructureSubst]
k:70 [in GMuAnnot.InfrastructureOpen]
k:73 [in GMuAnnot.InfrastructureOpen]
k:74 [in GMuAnnot.InfrastructureSubst]
k:74 [in GMuAnnot.InfrastructureFV]
k:76 [in GMuAnnot.InfrastructureFV]
k:76 [in GMuAnnot.InfrastructureOpen]
k:80 [in GMuAnnot.InfrastructureOpen]
k:81 [in GMuAnnot.Definitions]
k:84 [in GMuAnnot.InfrastructureOpen]
k:87 [in GMuAnnot.InfrastructureSubst]
k:88 [in GMuAnnot.Definitions]
k:89 [in GMuAnnot.InfrastructureOpen]
k:94 [in GMuAnnot.InfrastructureOpen]
L
la:163 [in GMuAnnot.Prelude]lb:164 [in GMuAnnot.Prelude]
len:74 [in GMuAnnot.Prelude]
list_clause_ind:65 [in GMuAnnot.Definitions]
ls:105 [in GMuAnnot.InfrastructureFV]
ls:114 [in GMuAnnot.Prelude]
ls:14 [in GMuAnnot.InfrastructureFV]
ls:24 [in GMuAnnot.InfrastructureFV]
ls:3 [in GMuAnnot.InfrastructureFV]
ls:30 [in GMuAnnot.InfrastructureFV]
ls:38 [in GMuAnnot.InfrastructureFV]
ls:44 [in GMuAnnot.InfrastructureFV]
ls:46 [in GMuAnnot.Prelude]
ls:59 [in GMuAnnot.Prelude]
ls:67 [in GMuAnnot.Definitions]
ls:9 [in GMuAnnot.InfrastructureFV]
l1:174 [in GMuAnnot.Prelude]
l2:175 [in GMuAnnot.Prelude]
l:127 [in GMuAnnot.Prelude]
L:128 [in GMuAnnot.Definitions]
L:131 [in GMuAnnot.Prelude]
L:134 [in GMuAnnot.Definitions]
L:140 [in GMuAnnot.Definitions]
L:145 [in GMuAnnot.Definitions]
L:149 [in GMuAnnot.Definitions]
l:179 [in GMuAnnot.Prelude]
L:207 [in GMuAnnot.Definitions]
L:225 [in GMuAnnot.Definitions]
L:265 [in GMuAnnot.Definitions]
L:274 [in GMuAnnot.Definitions]
L:285 [in GMuAnnot.Definitions]
l:347 [in GMuAnnot.Definitions]
l:52 [in GMuAnnot.Prelude]
L:69 [in GMuAnnot.Prelude]
L:72 [in GMuAnnot.Prelude]
L:73 [in GMuAnnot.Prelude]
l:84 [in GMuAnnot.Prelude]
M
ms:152 [in GMuAnnot.Definitions]ms:290 [in GMuAnnot.Definitions]
ms:339 [in GMuAnnot.Definitions]
ms:376 [in GMuAnnot.Definitions]
ms:83 [in GMuAnnot.InfrastructureOpen]
m:11 [in GMuAnnot.Prelude]
N
Name:119 [in GMuAnnot.Definitions]Name:167 [in GMuAnnot.Definitions]
Name:18 [in GMuAnnot.CanonicalForms]
Name:196 [in GMuAnnot.Definitions]
Name:293 [in GMuAnnot.Definitions]
Name:5 [in GMuAnnot.CanonicalForms]
Name:91 [in GMuAnnot.Regularity]
n:10 [in GMuAnnot.InfrastructureOpen]
n:103 [in GMuAnnot.InfrastructureOpen]
n:104 [in GMuAnnot.InfrastructureOpen]
n:107 [in GMuAnnot.InfrastructureOpen]
n:110 [in GMuAnnot.InfrastructureOpen]
n:113 [in GMuAnnot.InfrastructureOpen]
n:12 [in GMuAnnot.Definitions]
n:13 [in GMuAnnot.Prelude]
N:137 [in GMuAnnot.InfrastructureOpen]
n:15 [in GMuAnnot.Prelude]
n:18 [in GMuAnnot.Prelude]
n:180 [in GMuAnnot.Prelude]
N:19 [in GMuAnnot.InfrastructureSubstPrim]
n:20 [in GMuAnnot.Prelude]
n:22 [in GMuAnnot.Prelude]
n:25 [in GMuAnnot.Prelude]
N:29 [in GMuAnnot.InfrastructureOpen]
n:3 [in GMuAnnot.InfrastructureOpen]
n:30 [in GMuAnnot.Prelude]
n:33 [in GMuAnnot.Prelude]
n:34 [in GMuAnnot.InfrastructureOpen]
n:35 [in GMuAnnot.Prelude]
n:37 [in GMuAnnot.Prelude]
n:38 [in GMuAnnot.InfrastructureOpen]
n:40 [in GMuAnnot.Prelude]
N:44 [in GMuAnnot.CanonicalForms]
n:7 [in GMuAnnot.InfrastructureOpen]
N:78 [in GMuAnnot.InfrastructureOpen]
n:8 [in GMuAnnot.InfrastructureSubst]
n:90 [in GMuAnnot.InfrastructureOpen]
N:91 [in GMuAnnot.Equations]
n:95 [in GMuAnnot.InfrastructureOpen]
N:97 [in GMuAnnot.InfrastructureOpen]
n:98 [in GMuAnnot.InfrastructureOpen]
O
OTs:135 [in GMuAnnot.InfrastructureOpen]O1:130 [in GMuAnnot.SubstMatch]
O1:140 [in GMuAnnot.SubstMatch]
O1:146 [in GMuAnnot.InfrastructureFV]
O1:146 [in GMuAnnot.SubstMatch]
O1:160 [in GMuAnnot.SubstMatch]
O1:173 [in GMuAnnot.SubstMatch]
O1:175 [in GMuAnnot.InfrastructureFV]
O1:186 [in GMuAnnot.SubstMatch]
O1:194 [in GMuAnnot.SubstMatch]
O1:20 [in GMuAnnot.SubstMatch]
O1:219 [in GMuAnnot.SubstMatch]
O1:238 [in GMuAnnot.SubstMatch]
O1:27 [in GMuAnnot.SubstMatch]
O1:38 [in GMuAnnot.SubstMatch]
O2:141 [in GMuAnnot.SubstMatch]
O2:147 [in GMuAnnot.InfrastructureFV]
O2:147 [in GMuAnnot.SubstMatch]
O2:174 [in GMuAnnot.SubstMatch]
O2:176 [in GMuAnnot.InfrastructureFV]
O2:187 [in GMuAnnot.SubstMatch]
O2:195 [in GMuAnnot.SubstMatch]
O2:220 [in GMuAnnot.SubstMatch]
O2:239 [in GMuAnnot.SubstMatch]
O2:29 [in GMuAnnot.SubstMatch]
O:103 [in GMuAnnot.SubstMatch]
O:108 [in GMuAnnot.SubstMatch]
O:11 [in GMuAnnot.InfrastructureSubstPrim]
O:114 [in GMuAnnot.SubstMatch]
O:119 [in GMuAnnot.SubstMatch]
O:123 [in GMuAnnot.SubstMatch]
O:14 [in GMuAnnot.InfrastructureSubstPrim]
O:143 [in GMuAnnot.InfrastructureFV]
O:148 [in GMuAnnot.InfrastructureFV]
O:17 [in GMuAnnot.InfrastructureSubstPrim]
O:178 [in GMuAnnot.InfrastructureFV]
O:181 [in GMuAnnot.SubstMatch]
O:193 [in GMuAnnot.SubstMatch]
O:21 [in GMuAnnot.InfrastructureSubstPrim]
O:22 [in GMuAnnot.InfrastructureSubstPrim]
O:231 [in GMuAnnot.SubstMatch]
O:86 [in GMuAnnot.SubstMatch]
O:9 [in GMuAnnot.InfrastructureSubstPrim]
O:93 [in GMuAnnot.SubstMatch]
O:97 [in GMuAnnot.SubstMatch]
P
Ph:134 [in GMuAnnot.Prelude]Ps:146 [in GMuAnnot.Preservation]
Ps:173 [in GMuAnnot.InfrastructureSubst]
Ps:177 [in GMuAnnot.InfrastructureSubst]
Pts:135 [in GMuAnnot.Prelude]
P:10 [in GMuAnnot.Prelude]
P:104 [in GMuAnnot.InfrastructureFV]
P:106 [in GMuAnnot.SubstMatch]
P:111 [in GMuAnnot.InfrastructureSubst]
P:111 [in GMuAnnot.SubstMatch]
P:113 [in GMuAnnot.InfrastructureFV]
P:114 [in GMuAnnot.InfrastructureSubst]
P:117 [in GMuAnnot.InfrastructureFV]
P:12 [in GMuAnnot.InfrastructureSubst]
P:125 [in GMuAnnot.Preservation]
P:125 [in GMuAnnot.InfrastructureSubst]
P:129 [in GMuAnnot.InfrastructureSubst]
P:130 [in GMuAnnot.InfrastructureFV]
P:135 [in GMuAnnot.Preservation]
P:135 [in GMuAnnot.InfrastructureSubst]
P:14 [in GMuAnnot.Prelude]
P:148 [in GMuAnnot.Preservation]
P:154 [in GMuAnnot.Preservation]
P:161 [in GMuAnnot.InfrastructureFV]
P:168 [in GMuAnnot.InfrastructureFV]
P:170 [in GMuAnnot.InfrastructureSubst]
P:173 [in GMuAnnot.Prelude]
P:180 [in GMuAnnot.InfrastructureFV]
P:182 [in GMuAnnot.InfrastructureSubst]
P:184 [in GMuAnnot.InfrastructureFV]
P:188 [in GMuAnnot.InfrastructureFV]
P:200 [in GMuAnnot.SubstMatch]
P:23 [in GMuAnnot.InfrastructureFV]
P:24 [in GMuAnnot.Prelude]
P:26 [in GMuAnnot.InfrastructureSubstPrim]
P:29 [in GMuAnnot.Prelude]
P:33 [in GMuAnnot.InfrastructureSubst]
P:38 [in GMuAnnot.Regularity2]
P:39 [in GMuAnnot.InfrastructureSubst]
P:39 [in GMuAnnot.Prelude]
P:4 [in GMuAnnot.InfrastructureFV]
P:44 [in GMuAnnot.Regularity2]
P:47 [in GMuAnnot.InfrastructureFV]
P:5 [in GMuAnnot.InfrastructureSubstPrim]
P:60 [in GMuAnnot.Regularity2]
P:60 [in GMuAnnot.Prelude]
P:69 [in GMuAnnot.Regularity2]
P:7 [in GMuAnnot.InfrastructureSubst]
P:82 [in GMuAnnot.InfrastructureSubst]
P:84 [in GMuAnnot.Regularity]
P:93 [in GMuAnnot.InfrastructureSubst]
P:98 [in GMuAnnot.InfrastructureSubst]
T
tail_proof:64 [in GMuAnnot.Definitions]Targ:204 [in GMuAnnot.Definitions]
Tarity:199 [in GMuAnnot.Definitions]
Tarity:295 [in GMuAnnot.Definitions]
Tarity:92 [in GMuAnnot.Regularity]
TA1:73 [in GMuAnnot.Equations]
TA1:79 [in GMuAnnot.Equations]
TA2:75 [in GMuAnnot.Equations]
TA2:81 [in GMuAnnot.Equations]
TB1:74 [in GMuAnnot.Equations]
TB1:80 [in GMuAnnot.Equations]
TB2:76 [in GMuAnnot.Equations]
TB2:82 [in GMuAnnot.Equations]
Tc:294 [in GMuAnnot.Definitions]
tc:33 [in GMuAnnot.Equations]
Tc:343 [in GMuAnnot.Definitions]
Tc:378 [in GMuAnnot.Definitions]
Tparams:118 [in GMuAnnot.Definitions]
Tparams:13 [in GMuAnnot.CanonicalForms]
Tparams:166 [in GMuAnnot.Definitions]
Tparams:4 [in GMuAnnot.CanonicalForms]
Tparams:91 [in GMuAnnot.InfrastructureSubst]
Tparam:121 [in GMuAnnot.Definitions]
Tparam:94 [in GMuAnnot.InfrastructureSubst]
Tparam:95 [in GMuAnnot.InfrastructureSubst]
Tret:205 [in GMuAnnot.Definitions]
TR:85 [in GMuAnnot.InfrastructureOpen]
Ts':45 [in GMuAnnot.CanonicalForms]
Ts:107 [in GMuAnnot.Regularity]
Ts:133 [in GMuAnnot.InfrastructureSubst]
Ts:155 [in GMuAnnot.InfrastructureFV]
Ts:159 [in GMuAnnot.InfrastructureSubst]
Ts:163 [in GMuAnnot.InfrastructureSubst]
Ts:168 [in GMuAnnot.Prelude]
Ts:18 [in GMuAnnot.Definitions]
Ts:18 [in GMuAnnot.InfrastructureSubstPrim]
Ts:192 [in GMuAnnot.Preservation]
Ts:195 [in GMuAnnot.Definitions]
Ts:196 [in GMuAnnot.Preservation]
Ts:210 [in GMuAnnot.SubstMatch]
Ts:28 [in GMuAnnot.InfrastructureOpen]
Ts:291 [in GMuAnnot.Definitions]
Ts:338 [in GMuAnnot.Definitions]
Ts:43 [in GMuAnnot.CanonicalForms]
Ts:61 [in GMuAnnot.Regularity2]
Ts:63 [in GMuAnnot.InfrastructureFV]
Ts:77 [in GMuAnnot.InfrastructureOpen]
Ts:79 [in GMuAnnot.InfrastructureFV]
Ts:89 [in GMuAnnot.Equations]
Ts:97 [in GMuAnnot.Equations]
Ts:98 [in GMuAnnot.InfrastructureFV]
Tts:126 [in GMuAnnot.InfrastructureSubst]
TT1:103 [in GMuAnnot.Preservation]
TT1:194 [in GMuAnnot.Definitions]
TT1:223 [in GMuAnnot.Definitions]
TT1:249 [in GMuAnnot.Definitions]
TT1:282 [in GMuAnnot.Definitions]
TT1:297 [in GMuAnnot.Definitions]
TT1:54 [in GMuAnnot.Preservation]
TT2:104 [in GMuAnnot.Preservation]
TT2:224 [in GMuAnnot.Definitions]
TT2:250 [in GMuAnnot.Definitions]
TT2:283 [in GMuAnnot.Definitions]
TT2:55 [in GMuAnnot.Preservation]
TT:103 [in GMuAnnot.InfrastructureFV]
TT:122 [in GMuAnnot.Regularity]
TT:127 [in GMuAnnot.Preservation]
TT:132 [in GMuAnnot.Regularity]
TT:136 [in GMuAnnot.Regularity]
TT:137 [in GMuAnnot.Preservation]
TT:147 [in GMuAnnot.Preservation]
TT:16 [in GMuAnnot.Preservation]
TT:163 [in GMuAnnot.Preservation]
TT:173 [in GMuAnnot.Preservation]
TT:182 [in GMuAnnot.Preservation]
TT:190 [in GMuAnnot.Preservation]
TT:214 [in GMuAnnot.Definitions]
TT:23 [in GMuAnnot.Preservation]
TT:231 [in GMuAnnot.Definitions]
TT:241 [in GMuAnnot.Definitions]
TT:257 [in GMuAnnot.Definitions]
TT:264 [in GMuAnnot.Definitions]
TT:271 [in GMuAnnot.Definitions]
TT:311 [in GMuAnnot.Definitions]
TT:32 [in GMuAnnot.Preservation]
TT:379 [in GMuAnnot.Definitions]
TT:384 [in GMuAnnot.Definitions]
TT:42 [in GMuAnnot.Preservation]
TT:57 [in GMuAnnot.Equations]
TT:63 [in GMuAnnot.Equations]
TT:8 [in GMuAnnot.Preservation]
TV:102 [in GMuAnnot.InfrastructureFV]
Typs:17 [in GMuAnnot.CanonicalForms]
Typs:9 [in GMuAnnot.CanonicalForms]
T':240 [in GMuAnnot.Definitions]
T':64 [in GMuAnnot.Equations]
T1:12 [in GMuAnnot.InfrastructureSubstPrim]
T1:124 [in GMuAnnot.Definitions]
T1:15 [in GMuAnnot.InfrastructureSubstPrim]
T1:162 [in GMuAnnot.Preservation]
T1:164 [in GMuAnnot.Definitions]
T1:172 [in GMuAnnot.Preservation]
T1:20 [in GMuAnnot.InfrastructureOpen]
T1:201 [in GMuAnnot.SubstMatch]
T1:212 [in GMuAnnot.SubstMatch]
T1:213 [in GMuAnnot.Definitions]
T1:216 [in GMuAnnot.SubstMatch]
T1:219 [in GMuAnnot.Definitions]
t1:22 [in GMuAnnot.Definitions]
T1:22 [in GMuAnnot.CanonicalForms]
T1:221 [in GMuAnnot.SubstMatch]
T1:23 [in GMuAnnot.InfrastructureOpen]
T1:230 [in GMuAnnot.Definitions]
T1:238 [in GMuAnnot.Definitions]
T1:24 [in GMuAnnot.Definitions]
T1:245 [in GMuAnnot.Definitions]
T1:247 [in GMuAnnot.SubstMatch]
T1:254 [in GMuAnnot.Definitions]
T1:261 [in GMuAnnot.Definitions]
T1:29 [in GMuAnnot.CanonicalForms]
T1:308 [in GMuAnnot.Definitions]
T1:326 [in GMuAnnot.Definitions]
T1:330 [in GMuAnnot.Definitions]
t1:34 [in GMuAnnot.Definitions]
T1:364 [in GMuAnnot.Definitions]
T1:369 [in GMuAnnot.Definitions]
T1:4 [in GMuAnnot.InfrastructureSubst]
T1:4 [in GMuAnnot.Progress]
T1:43 [in GMuAnnot.SubstMatch]
T1:48 [in GMuAnnot.SubstMatch]
t1:51 [in GMuAnnot.Definitions]
T1:55 [in GMuAnnot.Equations]
T1:57 [in GMuAnnot.InfrastructureOpen]
T1:61 [in GMuAnnot.SubstMatch]
T1:65 [in GMuAnnot.SubstMatch]
t1:66 [in GMuAnnot.InfrastructureSubst]
T1:72 [in GMuAnnot.InfrastructureFV]
T1:76 [in GMuAnnot.Regularity2]
T1:8 [in GMuAnnot.SubstMatch]
T1:82 [in GMuAnnot.SubstMatch]
T1:89 [in GMuAnnot.Regularity]
T1:9 [in GMuAnnot.InfrastructureSubst]
T2:10 [in GMuAnnot.InfrastructureSubst]
T2:125 [in GMuAnnot.Definitions]
T2:13 [in GMuAnnot.InfrastructureSubstPrim]
T2:16 [in GMuAnnot.InfrastructureSubstPrim]
T2:165 [in GMuAnnot.Definitions]
T2:166 [in GMuAnnot.Preservation]
T2:176 [in GMuAnnot.Preservation]
T2:18 [in GMuAnnot.InfrastructureSubst]
T2:202 [in GMuAnnot.SubstMatch]
T2:21 [in GMuAnnot.InfrastructureOpen]
T2:213 [in GMuAnnot.SubstMatch]
T2:217 [in GMuAnnot.SubstMatch]
T2:220 [in GMuAnnot.Definitions]
T2:222 [in GMuAnnot.SubstMatch]
t2:23 [in GMuAnnot.Definitions]
T2:23 [in GMuAnnot.CanonicalForms]
T2:24 [in GMuAnnot.InfrastructureOpen]
T2:246 [in GMuAnnot.Definitions]
T2:248 [in GMuAnnot.SubstMatch]
T2:25 [in GMuAnnot.Definitions]
T2:255 [in GMuAnnot.Definitions]
T2:262 [in GMuAnnot.Definitions]
T2:279 [in GMuAnnot.Definitions]
T2:30 [in GMuAnnot.CanonicalForms]
T2:309 [in GMuAnnot.Definitions]
T2:327 [in GMuAnnot.Definitions]
T2:331 [in GMuAnnot.Definitions]
t2:35 [in GMuAnnot.Definitions]
T2:365 [in GMuAnnot.Definitions]
T2:370 [in GMuAnnot.Definitions]
T2:44 [in GMuAnnot.SubstMatch]
T2:49 [in GMuAnnot.SubstMatch]
T2:5 [in GMuAnnot.InfrastructureSubst]
T2:5 [in GMuAnnot.Progress]
t2:52 [in GMuAnnot.Definitions]
T2:56 [in GMuAnnot.Equations]
T2:58 [in GMuAnnot.InfrastructureOpen]
T2:62 [in GMuAnnot.SubstMatch]
T2:66 [in GMuAnnot.SubstMatch]
t2:67 [in GMuAnnot.InfrastructureSubst]
T2:73 [in GMuAnnot.InfrastructureFV]
T2:77 [in GMuAnnot.Regularity2]
T2:83 [in GMuAnnot.SubstMatch]
T2:9 [in GMuAnnot.SubstMatch]
T:1 [in GMuAnnot.Progress]
T:10 [in GMuAnnot.InfrastructureSubstPrim]
T:101 [in GMuAnnot.InfrastructureFV]
T:102 [in GMuAnnot.Preservation]
T:102 [in GMuAnnot.Regularity]
T:106 [in GMuAnnot.InfrastructureOpen]
T:109 [in GMuAnnot.InfrastructureFV]
T:109 [in GMuAnnot.InfrastructureOpen]
T:110 [in GMuAnnot.InfrastructureFV]
T:111 [in GMuAnnot.Definitions]
T:111 [in GMuAnnot.Regularity]
T:112 [in GMuAnnot.Regularity]
T:112 [in GMuAnnot.InfrastructureOpen]
T:113 [in GMuAnnot.SubstMatch]
T:114 [in GMuAnnot.InfrastructureFV]
T:116 [in GMuAnnot.Regularity]
T:118 [in GMuAnnot.SubstMatch]
T:12 [in GMuAnnot.InfrastructureFV]
T:121 [in GMuAnnot.Regularity]
T:124 [in GMuAnnot.SubstMatch]
T:125 [in GMuAnnot.InfrastructureFV]
T:125 [in GMuAnnot.Prelude]
T:126 [in GMuAnnot.Preservation]
T:128 [in GMuAnnot.InfrastructureFV]
T:130 [in GMuAnnot.InfrastructureSubst]
T:131 [in GMuAnnot.Regularity]
T:136 [in GMuAnnot.Preservation]
T:137 [in GMuAnnot.Prelude]
T:138 [in GMuAnnot.Regularity]
T:138 [in GMuAnnot.InfrastructureOpen]
T:139 [in GMuAnnot.InfrastructureFV]
T:139 [in GMuAnnot.InfrastructureOpen]
T:141 [in GMuAnnot.Definitions]
T:141 [in GMuAnnot.InfrastructureOpen]
T:141 [in GMuAnnot.Prelude]
T:142 [in GMuAnnot.SubstMatch]
T:144 [in GMuAnnot.Prelude]
T:145 [in GMuAnnot.Preservation]
T:150 [in GMuAnnot.InfrastructureFV]
T:153 [in GMuAnnot.Definitions]
T:156 [in GMuAnnot.Prelude]
T:157 [in GMuAnnot.InfrastructureFV]
T:159 [in GMuAnnot.InfrastructureFV]
T:16 [in GMuAnnot.CanonicalForms]
T:16 [in GMuAnnot.InfrastructureSubst]
T:160 [in GMuAnnot.InfrastructureSubst]
T:166 [in GMuAnnot.InfrastructureFV]
T:17 [in GMuAnnot.Equations]
T:17 [in GMuAnnot.Regularity]
T:171 [in GMuAnnot.InfrastructureSubst]
T:183 [in GMuAnnot.Preservation]
T:183 [in GMuAnnot.InfrastructureSubst]
T:190 [in GMuAnnot.Definitions]
t:191 [in GMuAnnot.Prelude]
T:194 [in GMuAnnot.Preservation]
T:2 [in GMuAnnot.InfrastructureSubstPrim]
T:2 [in GMuAnnot.Progress]
T:20 [in GMuAnnot.InfrastructureSubstPrim]
T:201 [in GMuAnnot.Preservation]
T:206 [in GMuAnnot.Definitions]
T:21 [in GMuAnnot.InfrastructureSubst]
T:210 [in GMuAnnot.Preservation]
T:211 [in GMuAnnot.Preservation]
T:212 [in GMuAnnot.Preservation]
T:213 [in GMuAnnot.Preservation]
T:214 [in GMuAnnot.Preservation]
T:215 [in GMuAnnot.Preservation]
T:216 [in GMuAnnot.Preservation]
T:217 [in GMuAnnot.Preservation]
T:218 [in GMuAnnot.Preservation]
T:218 [in GMuAnnot.SubstMatch]
T:219 [in GMuAnnot.Preservation]
T:23 [in GMuAnnot.InfrastructureSubstPrim]
T:234 [in GMuAnnot.SubstMatch]
T:239 [in GMuAnnot.Definitions]
T:26 [in GMuAnnot.Regularity]
T:26 [in GMuAnnot.InfrastructureSubst]
T:26 [in GMuAnnot.InfrastructureOpen]
T:269 [in GMuAnnot.Definitions]
T:292 [in GMuAnnot.Definitions]
T:3 [in GMuAnnot.Equations]
T:3 [in GMuAnnot.Regularity]
T:3 [in GMuAnnot.InfrastructureSubst]
T:31 [in GMuAnnot.Definitions]
T:31 [in GMuAnnot.Regularity]
T:31 [in GMuAnnot.InfrastructureOpen]
T:314 [in GMuAnnot.Definitions]
T:319 [in GMuAnnot.Definitions]
T:332 [in GMuAnnot.Definitions]
T:35 [in GMuAnnot.CanonicalForms]
T:35 [in GMuAnnot.InfrastructureOpen]
T:356 [in GMuAnnot.Definitions]
T:36 [in GMuAnnot.InfrastructureOpen]
T:37 [in GMuAnnot.Regularity]
T:382 [in GMuAnnot.Definitions]
T:387 [in GMuAnnot.Definitions]
T:39 [in GMuAnnot.Regularity2]
T:40 [in GMuAnnot.Definitions]
T:40 [in GMuAnnot.InfrastructureOpen]
T:41 [in GMuAnnot.Preservation]
T:41 [in GMuAnnot.InfrastructureFV]
T:41 [in GMuAnnot.Prelude]
T:42 [in GMuAnnot.InfrastructureSubst]
T:42 [in GMuAnnot.Prelude]
T:43 [in GMuAnnot.Definitions]
T:43 [in GMuAnnot.Prelude]
T:45 [in GMuAnnot.Regularity2]
T:47 [in GMuAnnot.Regularity]
T:48 [in GMuAnnot.Definitions]
T:5 [in GMuAnnot.Equations]
T:51 [in GMuAnnot.InfrastructureFV]
T:51 [in GMuAnnot.Regularity2]
T:51 [in GMuAnnot.SubstMatch]
T:52 [in GMuAnnot.InfrastructureSubst]
T:53 [in GMuAnnot.Preservation]
T:53 [in GMuAnnot.Regularity]
t:54 [in GMuAnnot.Definitions]
T:54 [in GMuAnnot.InfrastructureFV]
T:54 [in GMuAnnot.Prelude]
T:57 [in GMuAnnot.InfrastructureFV]
T:58 [in GMuAnnot.Regularity2]
T:6 [in GMuAnnot.InfrastructureSubstPrim]
T:60 [in GMuAnnot.InfrastructureFV]
T:61 [in GMuAnnot.InfrastructureOpen]
T:62 [in GMuAnnot.Equations]
T:64 [in GMuAnnot.InfrastructureFV]
T:68 [in GMuAnnot.InfrastructureFV]
T:69 [in GMuAnnot.InfrastructureOpen]
T:70 [in GMuAnnot.InfrastructureFV]
T:71 [in GMuAnnot.Regularity]
T:72 [in GMuAnnot.InfrastructureOpen]
T:74 [in GMuAnnot.Regularity]
T:77 [in GMuAnnot.SubstMatch]
T:78 [in GMuAnnot.InfrastructureFV]
T:79 [in GMuAnnot.Regularity]
T:8 [in GMuAnnot.CanonicalForms]
T:8 [in GMuAnnot.Equations]
T:8 [in GMuAnnot.InfrastructureOpen]
T:82 [in GMuAnnot.InfrastructureFV]
t:83 [in GMuAnnot.Definitions]
T:85 [in GMuAnnot.Equations]
T:85 [in GMuAnnot.Regularity]
T:86 [in GMuAnnot.InfrastructureFV]
T:88 [in GMuAnnot.Prelude]
T:91 [in GMuAnnot.InfrastructureFV]
T:91 [in GMuAnnot.Prelude]
T:92 [in GMuAnnot.Equations]
t:95 [in GMuAnnot.Definitions]
T:96 [in GMuAnnot.InfrastructureSubst]
T:96 [in GMuAnnot.SubstMatch]
t:97 [in GMuAnnot.Definitions]
T:99 [in GMuAnnot.Equations]
T:99 [in GMuAnnot.InfrastructureFV]
U
Uh:31 [in GMuAnnot.InfrastructureSubst]Uh:37 [in GMuAnnot.InfrastructureSubst]
Us:100 [in GMuAnnot.Regularity]
Us:138 [in GMuAnnot.InfrastructureSubst]
Us:153 [in GMuAnnot.InfrastructureSubst]
Us:156 [in GMuAnnot.InfrastructureFV]
Us:169 [in GMuAnnot.Prelude]
Us:193 [in GMuAnnot.Preservation]
Us:198 [in GMuAnnot.Preservation]
Us:211 [in GMuAnnot.SubstMatch]
Us:43 [in GMuAnnot.InfrastructureSubst]
Us:62 [in GMuAnnot.Regularity2]
Us:90 [in GMuAnnot.Equations]
Us:98 [in GMuAnnot.Equations]
Ut:32 [in GMuAnnot.InfrastructureSubst]
Ut:38 [in GMuAnnot.InfrastructureSubst]
U0:110 [in GMuAnnot.Preservation]
U0:116 [in GMuAnnot.Preservation]
U0:137 [in GMuAnnot.SubstMatch]
U0:139 [in GMuAnnot.SubstMatch]
U0:154 [in GMuAnnot.SubstMatch]
U0:156 [in GMuAnnot.SubstMatch]
U0:167 [in GMuAnnot.SubstMatch]
U0:169 [in GMuAnnot.SubstMatch]
U0:226 [in GMuAnnot.SubstMatch]
U0:228 [in GMuAnnot.SubstMatch]
U0:61 [in GMuAnnot.Preservation]
U0:67 [in GMuAnnot.Preservation]
U0:73 [in GMuAnnot.Preservation]
U0:79 [in GMuAnnot.Preservation]
U0:87 [in GMuAnnot.Preservation]
U0:93 [in GMuAnnot.Preservation]
U1:184 [in GMuAnnot.Preservation]
U1:240 [in GMuAnnot.SubstMatch]
U1:245 [in GMuAnnot.SubstMatch]
U1:45 [in GMuAnnot.SubstMatch]
U2:185 [in GMuAnnot.Preservation]
U2:241 [in GMuAnnot.SubstMatch]
U2:246 [in GMuAnnot.SubstMatch]
U2:46 [in GMuAnnot.SubstMatch]
u:1 [in GMuAnnot.Preservation]
U:100 [in GMuAnnot.Equations]
U:100 [in GMuAnnot.Preservation]
U:103 [in GMuAnnot.Regularity]
U:108 [in GMuAnnot.Regularity]
U:11 [in GMuAnnot.Regularity]
U:116 [in GMuAnnot.InfrastructureOpen]
u:121 [in GMuAnnot.InfrastructureOpen]
U:123 [in GMuAnnot.InfrastructureSubst]
u:126 [in GMuAnnot.InfrastructureOpen]
U:126 [in GMuAnnot.Prelude]
U:126 [in GMuAnnot.SubstMatch]
U:128 [in GMuAnnot.InfrastructureSubst]
U:129 [in GMuAnnot.InfrastructureFV]
U:129 [in GMuAnnot.SubstMatch]
u:130 [in GMuAnnot.InfrastructureOpen]
U:131 [in GMuAnnot.InfrastructureSubst]
u:132 [in GMuAnnot.InfrastructureOpen]
U:135 [in GMuAnnot.SubstMatch]
U:136 [in GMuAnnot.InfrastructureSubst]
U:14 [in GMuAnnot.Preservation]
U:145 [in GMuAnnot.InfrastructureFV]
U:145 [in GMuAnnot.SubstMatch]
U:15 [in GMuAnnot.Equations]
U:15 [in GMuAnnot.InfrastructureSubst]
U:152 [in GMuAnnot.SubstMatch]
U:156 [in GMuAnnot.InfrastructureSubst]
U:157 [in GMuAnnot.InfrastructureSubst]
U:158 [in GMuAnnot.InfrastructureFV]
U:159 [in GMuAnnot.SubstMatch]
U:16 [in GMuAnnot.Regularity]
U:160 [in GMuAnnot.InfrastructureFV]
U:165 [in GMuAnnot.Preservation]
U:165 [in GMuAnnot.SubstMatch]
U:17 [in GMuAnnot.SubstMatch]
U:170 [in GMuAnnot.Definitions]
U:172 [in GMuAnnot.SubstMatch]
U:175 [in GMuAnnot.Preservation]
u:176 [in GMuAnnot.Definitions]
U:179 [in GMuAnnot.SubstMatch]
U:18 [in GMuAnnot.Equations]
U:180 [in GMuAnnot.InfrastructureSubst]
U:189 [in GMuAnnot.SubstMatch]
U:19 [in GMuAnnot.InfrastructureSubst]
U:195 [in GMuAnnot.Preservation]
U:2 [in GMuAnnot.InfrastructureSubst]
U:204 [in GMuAnnot.SubstMatch]
U:206 [in GMuAnnot.SubstMatch]
u:21 [in GMuAnnot.Preservation]
U:22 [in GMuAnnot.Preservation]
U:22 [in GMuAnnot.SubstMatch]
U:24 [in GMuAnnot.InfrastructureSubstPrim]
U:28 [in GMuAnnot.SubstMatch]
u:30 [in GMuAnnot.Preservation]
U:31 [in GMuAnnot.Preservation]
U:34 [in GMuAnnot.InfrastructureSubst]
U:35 [in GMuAnnot.InfrastructureSubst]
U:37 [in GMuAnnot.InfrastructureOpen]
U:39 [in GMuAnnot.SubstMatch]
U:40 [in GMuAnnot.InfrastructureSubst]
U:41 [in GMuAnnot.InfrastructureOpen]
U:46 [in GMuAnnot.InfrastructureSubst]
U:47 [in GMuAnnot.InfrastructureSubst]
U:49 [in GMuAnnot.InfrastructureSubst]
u:50 [in GMuAnnot.Preservation]
U:51 [in GMuAnnot.Preservation]
U:52 [in GMuAnnot.InfrastructureFV]
U:53 [in GMuAnnot.SubstMatch]
U:54 [in GMuAnnot.InfrastructureSubst]
U:55 [in GMuAnnot.InfrastructureFV]
U:57 [in GMuAnnot.InfrastructureSubst]
U:57 [in GMuAnnot.SubstMatch]
U:58 [in GMuAnnot.InfrastructureFV]
U:59 [in GMuAnnot.Regularity]
U:6 [in GMuAnnot.Equations]
U:6 [in GMuAnnot.Preservation]
U:60 [in GMuAnnot.InfrastructureSubst]
U:61 [in GMuAnnot.InfrastructureFV]
U:63 [in GMuAnnot.Regularity2]
u:64 [in GMuAnnot.InfrastructureSubst]
u:68 [in GMuAnnot.InfrastructureSubst]
U:68 [in GMuAnnot.SubstMatch]
U:70 [in GMuAnnot.Equations]
U:70 [in GMuAnnot.SubstMatch]
u:75 [in GMuAnnot.InfrastructureSubst]
u:79 [in GMuAnnot.InfrastructureSubst]
U:8 [in GMuAnnot.InfrastructureSubstPrim]
u:82 [in GMuAnnot.Definitions]
U:86 [in GMuAnnot.Equations]
U:88 [in GMuAnnot.Regularity]
u:88 [in GMuAnnot.InfrastructureSubst]
U:88 [in GMuAnnot.SubstMatch]
u:89 [in GMuAnnot.Definitions]
U:9 [in GMuAnnot.Equations]
u:9 [in GMuAnnot.Preservation]
U:93 [in GMuAnnot.Equations]
U:96 [in GMuAnnot.Definitions]
u:98 [in GMuAnnot.Definitions]
u:99 [in GMuAnnot.Preservation]
V
vk0:109 [in GMuAnnot.Preservation]vk0:115 [in GMuAnnot.Preservation]
vk0:60 [in GMuAnnot.Preservation]
vk0:66 [in GMuAnnot.Preservation]
vk0:72 [in GMuAnnot.Preservation]
vk0:78 [in GMuAnnot.Preservation]
vk0:86 [in GMuAnnot.Preservation]
vk0:92 [in GMuAnnot.Preservation]
vk:10 [in GMuAnnot.Regularity]
vk:116 [in GMuAnnot.Definitions]
vk:124 [in GMuAnnot.InfrastructureFV]
vk:161 [in GMuAnnot.Preservation]
vk:166 [in GMuAnnot.InfrastructureSubst]
vk:171 [in GMuAnnot.Preservation]
vk:189 [in GMuAnnot.Definitions]
vk:4 [in GMuAnnot.InfrastructureOpen]
vk:46 [in GMuAnnot.Regularity]
vk:48 [in GMuAnnot.InfrastructureOpen]
vk:50 [in GMuAnnot.Regularity2]
vk:52 [in GMuAnnot.Regularity]
vk:57 [in GMuAnnot.Regularity2]
vk:58 [in GMuAnnot.Regularity]
vk:70 [in GMuAnnot.Regularity]
vk:71 [in GMuAnnot.InfrastructureSubst]
vk:75 [in GMuAnnot.Regularity2]
vk:77 [in GMuAnnot.InfrastructureSubst]
vk:83 [in GMuAnnot.InfrastructureSubst]
vk:85 [in GMuAnnot.InfrastructureFV]
vk:90 [in GMuAnnot.InfrastructureFV]
vk:93 [in GMuAnnot.InfrastructureOpen]
Vs:199 [in GMuAnnot.Preservation]
v1:109 [in GMuAnnot.Prelude]
V1:132 [in GMuAnnot.SubstMatch]
v1:138 [in GMuAnnot.Definitions]
v1:142 [in GMuAnnot.Definitions]
V1:149 [in GMuAnnot.SubstMatch]
V1:162 [in GMuAnnot.SubstMatch]
V1:176 [in GMuAnnot.SubstMatch]
v1:24 [in GMuAnnot.CanonicalForms]
v1:31 [in GMuAnnot.CanonicalForms]
v1:321 [in GMuAnnot.Definitions]
v1:324 [in GMuAnnot.Definitions]
v1:328 [in GMuAnnot.Definitions]
v1:351 [in GMuAnnot.Definitions]
v1:36 [in GMuAnnot.CanonicalForms]
v1:366 [in GMuAnnot.Definitions]
v2:110 [in GMuAnnot.Prelude]
V2:133 [in GMuAnnot.SubstMatch]
V2:150 [in GMuAnnot.SubstMatch]
V2:163 [in GMuAnnot.SubstMatch]
V2:177 [in GMuAnnot.SubstMatch]
v2:25 [in GMuAnnot.CanonicalForms]
v2:316 [in GMuAnnot.Definitions]
v2:325 [in GMuAnnot.Definitions]
v2:329 [in GMuAnnot.Definitions]
V:10 [in GMuAnnot.Equations]
V:101 [in GMuAnnot.InfrastructureSubst]
v:106 [in GMuAnnot.InfrastructureSubst]
v:120 [in GMuAnnot.InfrastructureOpen]
V:125 [in GMuAnnot.InfrastructureOpen]
V:129 [in GMuAnnot.Definitions]
V:139 [in GMuAnnot.Definitions]
V:143 [in GMuAnnot.InfrastructureSubst]
V:149 [in GMuAnnot.InfrastructureSubst]
V:158 [in GMuAnnot.Definitions]
V:191 [in GMuAnnot.Preservation]
V:211 [in GMuAnnot.Definitions]
V:22 [in GMuAnnot.InfrastructureSubst]
v:270 [in GMuAnnot.Definitions]
V:278 [in GMuAnnot.Definitions]
V:28 [in GMuAnnot.InfrastructureSubst]
V:31 [in GMuAnnot.SubstMatch]
v:333 [in GMuAnnot.Definitions]
v:47 [in GMuAnnot.CanonicalForms]
X
Xs:104 [in GMuAnnot.InfrastructureSubst]Xs:131 [in GMuAnnot.InfrastructureFV]
Xs:137 [in GMuAnnot.InfrastructureSubst]
Xs:141 [in GMuAnnot.InfrastructureSubst]
Xs:146 [in GMuAnnot.InfrastructureSubst]
Xs:151 [in GMuAnnot.InfrastructureSubst]
Xs:20 [in GMuAnnot.InfrastructureSubst]
Xs:25 [in GMuAnnot.InfrastructureSubst]
Xs:41 [in GMuAnnot.InfrastructureSubst]
Xs:99 [in GMuAnnot.InfrastructureSubst]
x0:108 [in GMuAnnot.Preservation]
x0:114 [in GMuAnnot.Preservation]
X0:136 [in GMuAnnot.SubstMatch]
X0:138 [in GMuAnnot.SubstMatch]
X0:153 [in GMuAnnot.SubstMatch]
X0:155 [in GMuAnnot.SubstMatch]
X0:166 [in GMuAnnot.SubstMatch]
X0:168 [in GMuAnnot.SubstMatch]
x0:59 [in GMuAnnot.Preservation]
x0:65 [in GMuAnnot.Preservation]
x0:71 [in GMuAnnot.Preservation]
x0:77 [in GMuAnnot.Preservation]
x0:85 [in GMuAnnot.Preservation]
x0:91 [in GMuAnnot.Preservation]
x:101 [in GMuAnnot.InfrastructureOpen]
x:102 [in GMuAnnot.InfrastructureOpen]
X:103 [in GMuAnnot.InfrastructureSubst]
X:105 [in GMuAnnot.Preservation]
x:106 [in GMuAnnot.Prelude]
X:107 [in GMuAnnot.InfrastructureFV]
x:108 [in GMuAnnot.Prelude]
X:11 [in GMuAnnot.InfrastructureSubst]
x:11 [in GMuAnnot.InfrastructureOpen]
X:111 [in GMuAnnot.Preservation]
X:111 [in GMuAnnot.InfrastructureFV]
X:115 [in GMuAnnot.Regularity]
X:115 [in GMuAnnot.InfrastructureFV]
x:117 [in GMuAnnot.Definitions]
x:12 [in GMuAnnot.InfrastructureOpen]
x:120 [in GMuAnnot.InfrastructureFV]
X:123 [in GMuAnnot.Regularity]
x:123 [in GMuAnnot.InfrastructureFV]
x:123 [in GMuAnnot.Prelude]
X:124 [in GMuAnnot.Regularity]
X:125 [in GMuAnnot.SubstMatch]
X:127 [in GMuAnnot.InfrastructureFV]
X:128 [in GMuAnnot.Preservation]
X:129 [in GMuAnnot.Preservation]
X:13 [in GMuAnnot.InfrastructureSubst]
X:13 [in GMuAnnot.Regularity2]
x:130 [in GMuAnnot.Prelude]
x:131 [in GMuAnnot.Definitions]
X:131 [in GMuAnnot.SubstMatch]
x:134 [in GMuAnnot.InfrastructureFV]
X:134 [in GMuAnnot.SubstMatch]
X:136 [in GMuAnnot.Definitions]
x:136 [in GMuAnnot.InfrastructureFV]
X:137 [in GMuAnnot.Definitions]
X:14 [in GMuAnnot.Equations]
x:143 [in GMuAnnot.Definitions]
x:144 [in GMuAnnot.Definitions]
X:144 [in GMuAnnot.InfrastructureFV]
X:145 [in GMuAnnot.InfrastructureSubst]
x:145 [in GMuAnnot.Prelude]
x:148 [in GMuAnnot.Definitions]
x:148 [in GMuAnnot.Prelude]
X:148 [in GMuAnnot.SubstMatch]
x:15 [in GMuAnnot.Definitions]
X:150 [in GMuAnnot.InfrastructureSubst]
x:150 [in GMuAnnot.Prelude]
X:151 [in GMuAnnot.SubstMatch]
x:152 [in GMuAnnot.Prelude]
X:154 [in GMuAnnot.InfrastructureSubst]
x:154 [in GMuAnnot.Prelude]
X:155 [in GMuAnnot.InfrastructureSubst]
x:156 [in GMuAnnot.Definitions]
x:160 [in GMuAnnot.Preservation]
x:161 [in GMuAnnot.Definitions]
X:161 [in GMuAnnot.SubstMatch]
X:164 [in GMuAnnot.SubstMatch]
x:165 [in GMuAnnot.InfrastructureSubst]
x:165 [in GMuAnnot.InfrastructureFV]
X:17 [in GMuAnnot.InfrastructureSubst]
X:17 [in GMuAnnot.InfrastructureOpen]
x:170 [in GMuAnnot.Preservation]
x:172 [in GMuAnnot.InfrastructureFV]
X:175 [in GMuAnnot.SubstMatch]
X:178 [in GMuAnnot.SubstMatch]
X:179 [in GMuAnnot.InfrastructureSubst]
X:18 [in GMuAnnot.Regularity]
x:185 [in GMuAnnot.InfrastructureFV]
x:188 [in GMuAnnot.Definitions]
X:188 [in GMuAnnot.SubstMatch]
x:19 [in GMuAnnot.Equations]
x:2 [in GMuAnnot.InfrastructureFV]
x:2 [in GMuAnnot.InfrastructureOpen]
x:2 [in GMuAnnot.Prelude]
X:20 [in GMuAnnot.Regularity]
x:202 [in GMuAnnot.Preservation]
x:203 [in GMuAnnot.Preservation]
X:203 [in GMuAnnot.SubstMatch]
x:204 [in GMuAnnot.Preservation]
x:205 [in GMuAnnot.Preservation]
X:205 [in GMuAnnot.SubstMatch]
x:206 [in GMuAnnot.Preservation]
x:207 [in GMuAnnot.Preservation]
x:21 [in GMuAnnot.Equations]
X:21 [in GMuAnnot.SubstMatch]
x:215 [in GMuAnnot.Definitions]
x:220 [in GMuAnnot.Preservation]
x:221 [in GMuAnnot.Preservation]
X:225 [in GMuAnnot.SubstMatch]
X:227 [in GMuAnnot.SubstMatch]
x:23 [in GMuAnnot.Equations]
X:232 [in GMuAnnot.Definitions]
X:233 [in GMuAnnot.Definitions]
X:24 [in GMuAnnot.InfrastructureSubst]
x:25 [in GMuAnnot.Equations]
X:25 [in GMuAnnot.SubstMatch]
x:272 [in GMuAnnot.Definitions]
x:273 [in GMuAnnot.Definitions]
x:284 [in GMuAnnot.Definitions]
X:29 [in GMuAnnot.InfrastructureSubst]
x:3 [in GMuAnnot.Prelude]
x:303 [in GMuAnnot.Definitions]
X:32 [in GMuAnnot.InfrastructureOpen]
X:36 [in GMuAnnot.SubstMatch]
x:37 [in GMuAnnot.InfrastructureFV]
x:4 [in GMuAnnot.Prelude]
X:44 [in GMuAnnot.InfrastructureSubst]
x:45 [in GMuAnnot.Regularity]
X:45 [in GMuAnnot.InfrastructureSubst]
x:46 [in GMuAnnot.InfrastructureFV]
x:47 [in GMuAnnot.InfrastructureOpen]
x:47 [in GMuAnnot.Prelude]
X:48 [in GMuAnnot.InfrastructureSubst]
x:49 [in GMuAnnot.Preservation]
x:49 [in GMuAnnot.Regularity2]
x:5 [in GMuAnnot.Prelude]
x:51 [in GMuAnnot.Regularity]
X:53 [in GMuAnnot.InfrastructureSubst]
X:55 [in GMuAnnot.InfrastructureSubst]
X:56 [in GMuAnnot.Preservation]
x:56 [in GMuAnnot.Regularity2]
X:56 [in GMuAnnot.SubstMatch]
x:57 [in GMuAnnot.Regularity]
X:59 [in GMuAnnot.InfrastructureSubst]
X:6 [in GMuAnnot.InfrastructureSubst]
x:6 [in GMuAnnot.InfrastructureOpen]
x:6 [in GMuAnnot.Prelude]
X:62 [in GMuAnnot.Preservation]
x:62 [in GMuAnnot.InfrastructureSubst]
X:65 [in GMuAnnot.Regularity]
X:65 [in GMuAnnot.InfrastructureFV]
X:67 [in GMuAnnot.InfrastructureFV]
X:67 [in GMuAnnot.SubstMatch]
X:68 [in GMuAnnot.Preservation]
x:68 [in GMuAnnot.Prelude]
x:69 [in GMuAnnot.Regularity]
X:7 [in GMuAnnot.InfrastructureSubstPrim]
x:7 [in GMuAnnot.Prelude]
x:70 [in GMuAnnot.InfrastructureSubst]
x:71 [in GMuAnnot.InfrastructureFV]
x:71 [in GMuAnnot.Prelude]
x:72 [in GMuAnnot.InfrastructureSubst]
X:74 [in GMuAnnot.Preservation]
x:74 [in GMuAnnot.Regularity2]
X:76 [in GMuAnnot.SubstMatch]
x:77 [in GMuAnnot.InfrastructureFV]
x:78 [in GMuAnnot.InfrastructureSubst]
x:8 [in GMuAnnot.InfrastructureFV]
x:8 [in GMuAnnot.Prelude]
x:81 [in GMuAnnot.InfrastructureFV]
X:82 [in GMuAnnot.Preservation]
x:84 [in GMuAnnot.InfrastructureSubst]
x:84 [in GMuAnnot.InfrastructureFV]
x:85 [in GMuAnnot.Prelude]
x:86 [in GMuAnnot.Prelude]
X:87 [in GMuAnnot.SubstMatch]
X:88 [in GMuAnnot.Preservation]
X:88 [in GMuAnnot.InfrastructureFV]
X:88 [in GMuAnnot.InfrastructureOpen]
x:89 [in GMuAnnot.InfrastructureFV]
x:89 [in GMuAnnot.Prelude]
x:9 [in GMuAnnot.Regularity]
X:9 [in GMuAnnot.InfrastructureOpen]
x:9 [in GMuAnnot.Prelude]
X:90 [in GMuAnnot.InfrastructureSubst]
X:91 [in GMuAnnot.SubstMatch]
x:92 [in GMuAnnot.InfrastructureOpen]
x:92 [in GMuAnnot.Prelude]
X:94 [in GMuAnnot.InfrastructureFV]
X:95 [in GMuAnnot.SubstMatch]
X:97 [in GMuAnnot.InfrastructureFV]
x:97 [in GMuAnnot.Prelude]
x:98 [in GMuAnnot.Preservation]
X:98 [in GMuAnnot.SubstMatch]
Y
Y:102 [in GMuAnnot.InfrastructureSubst]y:107 [in GMuAnnot.InfrastructureSubst]
y:124 [in GMuAnnot.Prelude]
Y:13 [in GMuAnnot.SubstMatch]
Y:14 [in GMuAnnot.InfrastructureSubst]
Y:144 [in GMuAnnot.InfrastructureSubst]
Y:148 [in GMuAnnot.InfrastructureSubst]
Y:15 [in GMuAnnot.Preservation]
Y:23 [in GMuAnnot.InfrastructureSubst]
Y:27 [in GMuAnnot.InfrastructureSubst]
Y:30 [in GMuAnnot.SubstMatch]
Y:50 [in GMuAnnot.SubstMatch]
Y:56 [in GMuAnnot.InfrastructureSubst]
Y:66 [in GMuAnnot.InfrastructureFV]
Y:68 [in GMuAnnot.Equations]
y:73 [in GMuAnnot.InfrastructureSubst]
Y:81 [in GMuAnnot.SubstMatch]
y:87 [in GMuAnnot.Prelude]
y:90 [in GMuAnnot.Prelude]
Z
z':62 [in GMuAnnot.Prelude]Z:1 [in GMuAnnot.InfrastructureSubst]
Z:106 [in GMuAnnot.InfrastructureFV]
Z:110 [in GMuAnnot.InfrastructureSubst]
Z:112 [in GMuAnnot.InfrastructureFV]
Z:113 [in GMuAnnot.InfrastructureSubst]
Z:116 [in GMuAnnot.InfrastructureSubst]
Z:116 [in GMuAnnot.InfrastructureFV]
z:117 [in GMuAnnot.Prelude]
Z:120 [in GMuAnnot.InfrastructureSubst]
Z:121 [in GMuAnnot.InfrastructureFV]
Z:123 [in GMuAnnot.Preservation]
Z:124 [in GMuAnnot.InfrastructureSubst]
Z:127 [in GMuAnnot.InfrastructureSubst]
Z:13 [in GMuAnnot.InfrastructureFV]
Z:132 [in GMuAnnot.InfrastructureSubst]
Z:133 [in GMuAnnot.Preservation]
Z:134 [in GMuAnnot.InfrastructureSubst]
Z:169 [in GMuAnnot.Definitions]
Z:169 [in GMuAnnot.InfrastructureSubst]
z:174 [in GMuAnnot.Definitions]
Z:179 [in GMuAnnot.InfrastructureFV]
Z:183 [in GMuAnnot.InfrastructureFV]
Z:185 [in GMuAnnot.InfrastructureSubst]
Z:187 [in GMuAnnot.InfrastructureFV]
Z:188 [in GMuAnnot.InfrastructureSubst]
Z:199 [in GMuAnnot.SubstMatch]
Z:21 [in GMuAnnot.InfrastructureFV]
Z:28 [in GMuAnnot.InfrastructureFV]
Z:36 [in GMuAnnot.InfrastructureFV]
Z:37 [in GMuAnnot.Regularity2]
Z:43 [in GMuAnnot.Regularity2]
z:45 [in GMuAnnot.InfrastructureFV]
Z:59 [in GMuAnnot.Regularity2]
z:61 [in GMuAnnot.Prelude]
Z:68 [in GMuAnnot.Regularity2]
Z:81 [in GMuAnnot.InfrastructureSubst]
Z:83 [in GMuAnnot.Regularity]
z:86 [in GMuAnnot.InfrastructureSubst]
Z:92 [in GMuAnnot.InfrastructureSubst]
Z:97 [in GMuAnnot.InfrastructureSubst]
other
Δ1:120 [in GMuAnnot.Preservation]Δ1:128 [in GMuAnnot.SubstMatch]
Δ1:144 [in GMuAnnot.SubstMatch]
Δ1:158 [in GMuAnnot.SubstMatch]
Δ1:171 [in GMuAnnot.SubstMatch]
Δ1:178 [in GMuAnnot.Preservation]
Δ1:184 [in GMuAnnot.SubstMatch]
Δ1:191 [in GMuAnnot.SubstMatch]
Δ1:197 [in GMuAnnot.SubstMatch]
Δ1:236 [in GMuAnnot.SubstMatch]
Δ1:243 [in GMuAnnot.SubstMatch]
Δ2:121 [in GMuAnnot.Preservation]
Δ2:141 [in GMuAnnot.Preservation]
Δ2:179 [in GMuAnnot.Preservation]
Δ2:185 [in GMuAnnot.SubstMatch]
Δ2:192 [in GMuAnnot.SubstMatch]
Δ2:198 [in GMuAnnot.SubstMatch]
Δ2:237 [in GMuAnnot.SubstMatch]
Δ2:244 [in GMuAnnot.SubstMatch]
Δ:101 [in GMuAnnot.Regularity]
Δ:104 [in GMuAnnot.Regularity]
Δ:104 [in GMuAnnot.SubstMatch]
Δ:109 [in GMuAnnot.SubstMatch]
Δ:11 [in GMuAnnot.CanonicalForms]
Δ:114 [in GMuAnnot.Regularity]
Δ:115 [in GMuAnnot.SubstMatch]
Δ:118 [in GMuAnnot.Regularity]
Δ:12 [in GMuAnnot.Equations]
Δ:120 [in GMuAnnot.SubstMatch]
Δ:122 [in GMuAnnot.SubstMatch]
Δ:126 [in GMuAnnot.InfrastructureFV]
Δ:128 [in GMuAnnot.Regularity]
Δ:131 [in GMuAnnot.Preservation]
Δ:134 [in GMuAnnot.Regularity]
Δ:138 [in GMuAnnot.InfrastructureFV]
Δ:140 [in GMuAnnot.Preservation]
Δ:157 [in GMuAnnot.Preservation]
Δ:16 [in GMuAnnot.Equations]
Δ:168 [in GMuAnnot.Preservation]
Δ:18 [in GMuAnnot.Preservation]
Δ:182 [in GMuAnnot.InfrastructureFV]
Δ:182 [in GMuAnnot.SubstMatch]
Δ:183 [in GMuAnnot.Definitions]
Δ:186 [in GMuAnnot.InfrastructureFV]
Δ:187 [in GMuAnnot.Definitions]
Δ:187 [in GMuAnnot.Preservation]
Δ:193 [in GMuAnnot.Definitions]
Δ:2 [in GMuAnnot.CanonicalForms]
Δ:2 [in GMuAnnot.Equations]
Δ:20 [in GMuAnnot.CanonicalForms]
Δ:208 [in GMuAnnot.SubstMatch]
Δ:209 [in GMuAnnot.Definitions]
Δ:215 [in GMuAnnot.SubstMatch]
Δ:217 [in GMuAnnot.Definitions]
Δ:227 [in GMuAnnot.Definitions]
Δ:235 [in GMuAnnot.Definitions]
Δ:243 [in GMuAnnot.Definitions]
Δ:252 [in GMuAnnot.Definitions]
Δ:259 [in GMuAnnot.Definitions]
Δ:267 [in GMuAnnot.Definitions]
Δ:27 [in GMuAnnot.CanonicalForms]
Δ:27 [in GMuAnnot.Preservation]
Δ:276 [in GMuAnnot.Definitions]
Δ:287 [in GMuAnnot.Definitions]
Δ:306 [in GMuAnnot.Definitions]
Δ:32 [in GMuAnnot.Equations]
Δ:33 [in GMuAnnot.CanonicalForms]
Δ:36 [in GMuAnnot.Preservation]
Δ:36 [in GMuAnnot.Regularity]
Δ:37 [in GMuAnnot.Equations]
Δ:38 [in GMuAnnot.CanonicalForms]
Δ:4 [in GMuAnnot.Equations]
Δ:40 [in GMuAnnot.Regularity]
Δ:41 [in GMuAnnot.CanonicalForms]
Δ:43 [in GMuAnnot.Regularity]
Δ:45 [in GMuAnnot.Equations]
Δ:46 [in GMuAnnot.Preservation]
Δ:47 [in GMuAnnot.Regularity2]
Δ:49 [in GMuAnnot.Regularity]
Δ:5 [in GMuAnnot.Regularity]
Δ:52 [in GMuAnnot.Equations]
Δ:53 [in GMuAnnot.Regularity2]
Δ:55 [in GMuAnnot.Regularity]
Δ:59 [in GMuAnnot.Equations]
Δ:66 [in GMuAnnot.Equations]
Δ:67 [in GMuAnnot.Regularity]
Δ:7 [in GMuAnnot.Equations]
Δ:71 [in GMuAnnot.Regularity2]
Δ:72 [in GMuAnnot.Equations]
Δ:73 [in GMuAnnot.Regularity]
Δ:78 [in GMuAnnot.Equations]
Δ:8 [in GMuAnnot.Regularity]
Δ:84 [in GMuAnnot.Equations]
Δ:87 [in GMuAnnot.Regularity]
Δ:88 [in GMuAnnot.Equations]
Δ:94 [in GMuAnnot.SubstMatch]
Δ:95 [in GMuAnnot.Preservation]
Θ1:15 [in GMuAnnot.SubstMatch]
Θ1:54 [in GMuAnnot.SubstMatch]
Θ1:63 [in GMuAnnot.SubstMatch]
Θ1:72 [in GMuAnnot.SubstMatch]
Θ2:16 [in GMuAnnot.SubstMatch]
Θ2:55 [in GMuAnnot.SubstMatch]
Θ2:64 [in GMuAnnot.SubstMatch]
Θ2:73 [in GMuAnnot.SubstMatch]
Θ:1 [in GMuAnnot.InfrastructureSubstPrim]
Θ:13 [in GMuAnnot.Equations]
Θ:14 [in GMuAnnot.SubstMatch]
Θ:3 [in GMuAnnot.InfrastructureSubstPrim]
Θ:3 [in GMuAnnot.SubstMatch]
Θ:31 [in GMuAnnot.Equations]
Θ:38 [in GMuAnnot.Equations]
Θ:41 [in GMuAnnot.Equations]
Θ:47 [in GMuAnnot.SubstMatch]
Θ:5 [in GMuAnnot.SubstMatch]
Θ:67 [in GMuAnnot.Equations]
Σ:1 [in GMuAnnot.CanonicalForms]
Σ:1 [in GMuAnnot.Regularity]
Σ:1 [in GMuAnnot.Regularity2]
Σ:1 [in GMuAnnot.SubstMatch]
Σ:10 [in GMuAnnot.CanonicalForms]
Σ:10 [in GMuAnnot.Preservation]
Σ:10 [in GMuAnnot.SubstMatch]
Σ:102 [in GMuAnnot.SubstMatch]
Σ:105 [in GMuAnnot.Regularity]
Σ:107 [in GMuAnnot.SubstMatch]
Σ:11 [in GMuAnnot.Equations]
Σ:112 [in GMuAnnot.SubstMatch]
Σ:113 [in GMuAnnot.Regularity]
Σ:117 [in GMuAnnot.Regularity]
Σ:117 [in GMuAnnot.SubstMatch]
Σ:119 [in GMuAnnot.Preservation]
Σ:121 [in GMuAnnot.SubstMatch]
Σ:127 [in GMuAnnot.Regularity]
Σ:127 [in GMuAnnot.SubstMatch]
Σ:13 [in GMuAnnot.Regularity]
Σ:130 [in GMuAnnot.Preservation]
Σ:133 [in GMuAnnot.Regularity]
Σ:137 [in GMuAnnot.InfrastructureFV]
Σ:139 [in GMuAnnot.Preservation]
Σ:14 [in GMuAnnot.Regularity2]
Σ:143 [in GMuAnnot.SubstMatch]
Σ:156 [in GMuAnnot.Preservation]
Σ:157 [in GMuAnnot.SubstMatch]
Σ:167 [in GMuAnnot.Preservation]
Σ:17 [in GMuAnnot.Preservation]
Σ:170 [in GMuAnnot.SubstMatch]
Σ:177 [in GMuAnnot.Preservation]
Σ:18 [in GMuAnnot.SubstMatch]
Σ:180 [in GMuAnnot.SubstMatch]
Σ:182 [in GMuAnnot.Definitions]
Σ:183 [in GMuAnnot.SubstMatch]
Σ:185 [in GMuAnnot.Definitions]
Σ:186 [in GMuAnnot.Preservation]
Σ:19 [in GMuAnnot.CanonicalForms]
Σ:19 [in GMuAnnot.Regularity2]
Σ:190 [in GMuAnnot.SubstMatch]
Σ:191 [in GMuAnnot.Definitions]
Σ:196 [in GMuAnnot.SubstMatch]
Σ:2 [in GMuAnnot.Preservation]
Σ:207 [in GMuAnnot.SubstMatch]
Σ:208 [in GMuAnnot.Definitions]
Σ:214 [in GMuAnnot.SubstMatch]
Σ:216 [in GMuAnnot.Definitions]
Σ:22 [in GMuAnnot.Regularity]
Σ:226 [in GMuAnnot.Definitions]
Σ:229 [in GMuAnnot.SubstMatch]
Σ:23 [in GMuAnnot.SubstMatch]
Σ:234 [in GMuAnnot.Definitions]
Σ:235 [in GMuAnnot.SubstMatch]
Σ:242 [in GMuAnnot.Definitions]
Σ:242 [in GMuAnnot.SubstMatch]
Σ:251 [in GMuAnnot.Definitions]
Σ:258 [in GMuAnnot.Definitions]
Σ:26 [in GMuAnnot.CanonicalForms]
Σ:26 [in GMuAnnot.Preservation]
Σ:26 [in GMuAnnot.Regularity2]
Σ:266 [in GMuAnnot.Definitions]
Σ:27 [in GMuAnnot.Regularity]
Σ:275 [in GMuAnnot.Definitions]
Σ:286 [in GMuAnnot.Definitions]
Σ:29 [in GMuAnnot.Equations]
Σ:3 [in GMuAnnot.Progress]
Σ:305 [in GMuAnnot.Definitions]
Σ:32 [in GMuAnnot.CanonicalForms]
Σ:34 [in GMuAnnot.Regularity]
Σ:34 [in GMuAnnot.Regularity2]
Σ:34 [in GMuAnnot.SubstMatch]
Σ:35 [in GMuAnnot.Preservation]
Σ:36 [in GMuAnnot.Equations]
Σ:37 [in GMuAnnot.CanonicalForms]
Σ:380 [in GMuAnnot.Definitions]
Σ:385 [in GMuAnnot.Definitions]
Σ:39 [in GMuAnnot.Regularity]
Σ:4 [in GMuAnnot.Regularity]
Σ:4 [in GMuAnnot.SubstMatch]
Σ:40 [in GMuAnnot.CanonicalForms]
Σ:40 [in GMuAnnot.Regularity2]
Σ:40 [in GMuAnnot.SubstMatch]
Σ:42 [in GMuAnnot.Regularity]
Σ:44 [in GMuAnnot.Equations]
Σ:45 [in GMuAnnot.Preservation]
Σ:46 [in GMuAnnot.Regularity2]
Σ:48 [in GMuAnnot.Regularity]
Σ:5 [in GMuAnnot.Regularity2]
Σ:50 [in GMuAnnot.Equations]
Σ:51 [in GMuAnnot.Equations]
Σ:52 [in GMuAnnot.Regularity2]
Σ:54 [in GMuAnnot.Regularity]
Σ:58 [in GMuAnnot.Equations]
Σ:58 [in GMuAnnot.SubstMatch]
Σ:61 [in GMuAnnot.Regularity]
Σ:64 [in GMuAnnot.Regularity2]
Σ:65 [in GMuAnnot.Equations]
Σ:66 [in GMuAnnot.Regularity]
Σ:7 [in GMuAnnot.Regularity]
Σ:70 [in GMuAnnot.Regularity2]
Σ:71 [in GMuAnnot.Equations]
Σ:71 [in GMuAnnot.SubstMatch]
Σ:72 [in GMuAnnot.Regularity]
Σ:75 [in GMuAnnot.Regularity]
Σ:77 [in GMuAnnot.Equations]
Σ:78 [in GMuAnnot.Regularity2]
Σ:78 [in GMuAnnot.SubstMatch]
Σ:80 [in GMuAnnot.Regularity]
Σ:83 [in GMuAnnot.Equations]
Σ:84 [in GMuAnnot.SubstMatch]
Σ:86 [in GMuAnnot.Regularity]
Σ:87 [in GMuAnnot.Equations]
Σ:9 [in GMuAnnot.Regularity2]
Σ:90 [in GMuAnnot.Regularity]
Σ:92 [in GMuAnnot.SubstMatch]
Σ:94 [in GMuAnnot.Preservation]
Σ:98 [in GMuAnnot.Regularity]
ϵ:142 [in GMuAnnot.InfrastructureFV]
ϵ:171 [in GMuAnnot.Prelude]
ϵ:25 [in GMuAnnot.Preservation]
ϵ:25 [in GMuAnnot.Regularity]
ϵ:25 [in GMuAnnot.Regularity2]
ϵ:33 [in GMuAnnot.Regularity]
Variable Index
M
ManyTest.T [in GMuAnnot.DefinitionsTests]S
SimpleEquationProperties.Σ [in GMuAnnot.Equations]T
trm_ind'.trm_let_case [in GMuAnnot.Definitions]trm_ind'.trm_match_case [in GMuAnnot.Definitions]
trm_ind'.trm_fix_case [in GMuAnnot.Definitions]
trm_ind'.trm_tapp_case [in GMuAnnot.Definitions]
trm_ind'.trm_tabs_case [in GMuAnnot.Definitions]
trm_ind'.trm_app_case [in GMuAnnot.Definitions]
trm_ind'.trm_abs_case [in GMuAnnot.Definitions]
trm_ind'.trm_snd_case [in GMuAnnot.Definitions]
trm_ind'.trm_fst_case [in GMuAnnot.Definitions]
trm_ind'.trm_tuple_case [in GMuAnnot.Definitions]
trm_ind'.trm_unit_case [in GMuAnnot.Definitions]
trm_ind'.trm_constructor_case [in GMuAnnot.Definitions]
trm_ind'.trm_fvar_case [in GMuAnnot.Definitions]
trm_ind'.trm_bvar_case [in GMuAnnot.Definitions]
trm_ind'.P [in GMuAnnot.Definitions]
Library Index
C
CanonicalFormsD
DefinitionsDefinitionsTests
E
EquationsI
InfrastructureInfrastructureFV
InfrastructureOpen
InfrastructureSubst
InfrastructureSubstPrim
N
NotationsP
PreludePreservation
Progress
R
RegularityRegularity2
S
SubstMatchConstructor Index
C
clause [in GMuAnnot.Definitions]closed_term_match [in GMuAnnot.InfrastructureOpen]
closed_term_constructor [in GMuAnnot.InfrastructureOpen]
closed_trm_let [in GMuAnnot.InfrastructureOpen]
closed_trm_fix [in GMuAnnot.InfrastructureOpen]
closed_trm_tapp [in GMuAnnot.InfrastructureOpen]
closed_trm_tabs [in GMuAnnot.InfrastructureOpen]
closed_trm_app [in GMuAnnot.InfrastructureOpen]
closed_trm_abs [in GMuAnnot.InfrastructureOpen]
closed_trm_tuple [in GMuAnnot.InfrastructureOpen]
closed_trm_snd [in GMuAnnot.InfrastructureOpen]
closed_trm_fst [in GMuAnnot.InfrastructureOpen]
closed_trm_unit [in GMuAnnot.InfrastructureOpen]
closed_trm_fvar [in GMuAnnot.InfrastructureOpen]
closed_trm_bvar [in GMuAnnot.InfrastructureOpen]
closed_typ_gadt [in GMuAnnot.InfrastructureOpen]
closed_typ_all [in GMuAnnot.InfrastructureOpen]
closed_typ_arrow [in GMuAnnot.InfrastructureOpen]
closed_typ_tuple [in GMuAnnot.InfrastructureOpen]
closed_typ_unit [in GMuAnnot.InfrastructureOpen]
closed_typ_fvar [in GMuAnnot.InfrastructureOpen]
closed_typ_bvar [in GMuAnnot.InfrastructureOpen]
E
ered_match [in GMuAnnot.Definitions]ered_let [in GMuAnnot.Definitions]
ered_tuple_snd [in GMuAnnot.Definitions]
ered_tuple_fst [in GMuAnnot.Definitions]
ered_snd [in GMuAnnot.Definitions]
ered_fst [in GMuAnnot.Definitions]
ered_tapp [in GMuAnnot.Definitions]
ered_app_2 [in GMuAnnot.Definitions]
ered_constructor [in GMuAnnot.Definitions]
ered_app_1 [in GMuAnnot.Definitions]
R
red_match [in GMuAnnot.Definitions]red_fix [in GMuAnnot.Definitions]
red_snd [in GMuAnnot.Definitions]
red_fst [in GMuAnnot.Definitions]
red_letbeta [in GMuAnnot.Definitions]
red_tbeta [in GMuAnnot.Definitions]
red_beta [in GMuAnnot.Definitions]
T
term_matchgadt [in GMuAnnot.Definitions]term_let [in GMuAnnot.Definitions]
term_fix [in GMuAnnot.Definitions]
term_tapp [in GMuAnnot.Definitions]
term_tabs [in GMuAnnot.Definitions]
term_app [in GMuAnnot.Definitions]
term_abs [in GMuAnnot.Definitions]
term_snd [in GMuAnnot.Definitions]
term_fst [in GMuAnnot.Definitions]
term_tuple [in GMuAnnot.Definitions]
term_unit [in GMuAnnot.Definitions]
term_constructor [in GMuAnnot.Definitions]
term_var [in GMuAnnot.Definitions]
trm_let [in GMuAnnot.Definitions]
trm_matchgadt [in GMuAnnot.Definitions]
trm_fix [in GMuAnnot.Definitions]
trm_tapp [in GMuAnnot.Definitions]
trm_tabs [in GMuAnnot.Definitions]
trm_app [in GMuAnnot.Definitions]
trm_abs [in GMuAnnot.Definitions]
trm_snd [in GMuAnnot.Definitions]
trm_fst [in GMuAnnot.Definitions]
trm_tuple [in GMuAnnot.Definitions]
trm_unit [in GMuAnnot.Definitions]
trm_constructor [in GMuAnnot.Definitions]
trm_fvar [in GMuAnnot.Definitions]
trm_bvar [in GMuAnnot.Definitions]
typing_eq [in GMuAnnot.Definitions]
typing_case [in GMuAnnot.Definitions]
typing_let [in GMuAnnot.Definitions]
typing_fix [in GMuAnnot.Definitions]
typing_snd [in GMuAnnot.Definitions]
typing_fst [in GMuAnnot.Definitions]
typing_tuple [in GMuAnnot.Definitions]
typing_tapp [in GMuAnnot.Definitions]
typing_tabs [in GMuAnnot.Definitions]
typing_app [in GMuAnnot.Definitions]
typing_abs [in GMuAnnot.Definitions]
typing_cons [in GMuAnnot.Definitions]
typing_var [in GMuAnnot.Definitions]
typing_unit [in GMuAnnot.Definitions]
V
value_gadt [in GMuAnnot.Definitions]value_tuple [in GMuAnnot.Definitions]
value_lamvar [in GMuAnnot.Definitions]
value_unit [in GMuAnnot.Definitions]
value_tabs [in GMuAnnot.Definitions]
value_abs [in GMuAnnot.Definitions]
Lemma Index
B
binds_ext [in GMuAnnot.Prelude]C
CanonicalConstructorType [in GMuAnnot.CanonicalForms]CanonicalConstructorTypeGen [in GMuAnnot.CanonicalForms]
CanonicalFormAbs [in GMuAnnot.CanonicalForms]
CanonicalFormGadt [in GMuAnnot.CanonicalForms]
CanonicalFormTAbs [in GMuAnnot.CanonicalForms]
CanonicalFormTuple [in GMuAnnot.CanonicalForms]
CanonicalFormUnit [in GMuAnnot.CanonicalForms]
closed_id [in GMuAnnot.InfrastructureOpen]
contradictory_env_test [in GMuAnnot.Equations]
contradictory_env_test_0 [in GMuAnnot.Equations]
D
distinct_split1 [in GMuAnnot.InfrastructureFV]domDelta_subst_td [in GMuAnnot.InfrastructureFV]
domDelta_app [in GMuAnnot.InfrastructureFV]
domDelta_in [in GMuAnnot.InfrastructureFV]
E
empty_is_not_contradictory [in GMuAnnot.Equations]empty_inter_implies_notin [in GMuAnnot.Prelude]
empty_eq_is_equivalent [in GMuAnnot.Progress]
entails_through_subst [in GMuAnnot.SubstMatch]
env_map_compose [in GMuAnnot.Prelude]
equations_from_lists_map [in GMuAnnot.Equations]
equations_have_no_dom [in GMuAnnot.InfrastructureFV]
equations_from_lists_are_equations [in GMuAnnot.Prelude]
equations_weaken_match [in GMuAnnot.SubstMatch]
equation_strengthen [in GMuAnnot.SubstMatch]
equation_weaken_var [in GMuAnnot.SubstMatch]
equation_weaken_eq [in GMuAnnot.SubstMatch]
eq_dec_var [in GMuAnnot.Prelude]
exist_alphas [in GMuAnnot.Prelude]
ext_in_map [in GMuAnnot.Prelude]
F
fold_left_subset [in GMuAnnot.InfrastructureFV]fold_left_subset_base [in GMuAnnot.InfrastructureFV]
fold_empty [in GMuAnnot.InfrastructureFV]
Forall2_eq_len [in GMuAnnot.Prelude]
from_list_spec2 [in GMuAnnot.Prelude]
from_list_spec [in GMuAnnot.Prelude]
fv_delta_equations [in GMuAnnot.InfrastructureFV]
fv_delta_alphas [in GMuAnnot.InfrastructureFV]
fv_delta_app [in GMuAnnot.InfrastructureFV]
fv_env_subst [in GMuAnnot.InfrastructureFV]
fv_subst_tt [in GMuAnnot.InfrastructureFV]
fv_env_extend [in GMuAnnot.InfrastructureFV]
fv_open_te_many [in GMuAnnot.InfrastructureFV]
fv_open_te [in GMuAnnot.InfrastructureFV]
fv_open_tt [in GMuAnnot.InfrastructureFV]
fv_smaller_many [in GMuAnnot.InfrastructureFV]
fv_typs_notin [in GMuAnnot.InfrastructureFV]
fv_smaller [in GMuAnnot.InfrastructureFV]
fv_open [in GMuAnnot.InfrastructureFV]
fv_fold_in [in GMuAnnot.InfrastructureFV]
fv_fold_in_clause [in GMuAnnot.InfrastructureFV]
fv_fold_in_general [in GMuAnnot.InfrastructureFV]
fv_fold_base_clause [in GMuAnnot.InfrastructureFV]
fv_fold_base [in GMuAnnot.InfrastructureFV]
fv_fold_general [in GMuAnnot.InfrastructureFV]
G
gadt_constructor_ok [in GMuAnnot.Regularity]H
helper_equations_commute [in GMuAnnot.Preservation]I
inversion_eq_typ_gadt [in GMuAnnot.Equations]inversion_eq_typ_all [in GMuAnnot.Equations]
inversion_eq_tuple [in GMuAnnot.Equations]
inversion_eq_arrow [in GMuAnnot.Equations]
inversion_typing_eq [in GMuAnnot.Equations]
inzip_map_clause_trm [in GMuAnnot.Prelude]
in_fold_exists [in GMuAnnot.InfrastructureFV]
in_domΔ_eq [in GMuAnnot.InfrastructureFV]
in_from_list [in GMuAnnot.Prelude]
is_var_defined_split [in GMuAnnot.SubstMatch]
is_var_defined_dom [in GMuAnnot.SubstMatch]
J
JMeq_from_eq [in GMuAnnot.Prelude]L
length_equality [in GMuAnnot.Prelude]LibList_mem [in GMuAnnot.Prelude]
LibList_map [in GMuAnnot.Prelude]
lists_map_eq [in GMuAnnot.Prelude]
list_fold_map [in GMuAnnot.Prelude]
M
map_map [in GMuAnnot.Prelude]map_id [in GMuAnnot.Prelude]
N
notin_from_list [in GMuAnnot.Equations]notin_fv_wf [in GMuAnnot.Regularity]
notin_domDelta_subst_td [in GMuAnnot.InfrastructureFV]
notin_env_binds [in GMuAnnot.InfrastructureFV]
notin_dom_tc_vars [in GMuAnnot.InfrastructureFV]
notin_domΔ_eq [in GMuAnnot.InfrastructureFV]
notin_env_inv [in GMuAnnot.InfrastructureFV]
notin_fv_tt_open [in GMuAnnot.InfrastructureFV]
notin_fold [in GMuAnnot.InfrastructureFV]
notin_inverse [in GMuAnnot.Prelude]
nth_error_map [in GMuAnnot.Prelude]
O
okt_is_type [in GMuAnnot.Regularity]okt_strengthen_delta_var [in GMuAnnot.Regularity]
okt_strengthen [in GMuAnnot.Regularity]
okt_is_wft [in GMuAnnot.Regularity]
okt_push_var_inv [in GMuAnnot.Regularity]
okt_implies_okgadt [in GMuAnnot.Regularity]
okt_is_ok [in GMuAnnot.Regularity]
okt_strengthen_delta_eq [in GMuAnnot.Regularity2]
okt_replace_typ [in GMuAnnot.Regularity2]
okt_through_subst_tdtb [in GMuAnnot.Regularity2]
okt_is_wft_2 [in GMuAnnot.Regularity2]
okt_push_fresh [in GMuAnnot.Regularity2]
okt_weakening_delta_many [in GMuAnnot.Regularity2]
okt_weakening_delta_many_eq [in GMuAnnot.Regularity2]
okt_weakening_delta_eq [in GMuAnnot.Regularity2]
okt_weakening_delta [in GMuAnnot.Regularity2]
okt_strengthen_simple [in GMuAnnot.Regularity2]
only_vars_is_tc_vars [in GMuAnnot.Equations]
opening_adds_one [in GMuAnnot.InfrastructureOpen]
open_te_many_test [in GMuAnnot.DefinitionsTests]
open_tt_many_test [in GMuAnnot.DefinitionsTests]
open_typlist_test [in GMuAnnot.DefinitionsTests]
open_ee_test [in GMuAnnot.DefinitionsTests]
open_te_test [in GMuAnnot.DefinitionsTests]
open_tt_test [in GMuAnnot.DefinitionsTests]
open_tt_many_closed [in GMuAnnot.InfrastructureOpen]
open_ee_rec_term [in GMuAnnot.InfrastructureOpen]
open_ee_rec_type_many [in GMuAnnot.InfrastructureOpen]
open_ee_rec_type_core [in GMuAnnot.InfrastructureOpen]
open_ee_rec_term_core [in GMuAnnot.InfrastructureOpen]
open_te_rec_term [in GMuAnnot.InfrastructureOpen]
open_tt_rec_type [in GMuAnnot.InfrastructureOpen]
open_tt_var_preserves_size [in GMuAnnot.InfrastructureOpen]
open_te_var_preserves_size [in GMuAnnot.InfrastructureOpen]
open_ee_var_preserves_size [in GMuAnnot.InfrastructureOpen]
P
preservation_thm [in GMuAnnot.Preservation]progress_thm [in GMuAnnot.Progress]
R
remove_true_equations [in GMuAnnot.Preservation]remove_true_equation [in GMuAnnot.Preservation]
rewrite_open_tt_many_gadt [in GMuAnnot.InfrastructureOpen]
S
sources_list_fst [in GMuAnnot.InfrastructureFV]sources_distinct [in GMuAnnot.SubstMatch]
spawn_unit_subst [in GMuAnnot.Equations]
split_notin_subset_union [in GMuAnnot.Prelude]
strong_induction_on_typ_size [in GMuAnnot.Prelude]
strong_induction_on_type_size_helper [in GMuAnnot.Prelude]
strong_induction_on_term_size [in GMuAnnot.Prelude]
strong_induction_on_term_size_helper [in GMuAnnot.Prelude]
strong_induction [in GMuAnnot.Prelude]
sublist_head_prop [in GMuAnnot.InfrastructureSubst]
sublist_tail_prop [in GMuAnnot.InfrastructureSubst]
subset_fold [in GMuAnnot.InfrastructureFV]
subset_transitive [in GMuAnnot.Prelude]
substitution_sources_from_in [in GMuAnnot.InfrastructureFV]
subst_has_no_fv2 [in GMuAnnot.Equations]
subst_ttΘ_into_tuple [in GMuAnnot.Equations]
subst_ttΘ_into_abs [in GMuAnnot.Equations]
subst_has_no_fv [in GMuAnnot.Equations]
subst_ee_fix_value [in GMuAnnot.InfrastructureSubst]
subst_ee_fix_term [in GMuAnnot.InfrastructureSubst]
subst_commute [in GMuAnnot.InfrastructureSubst]
subst_tb_many_id_on_fresh_env [in GMuAnnot.InfrastructureSubst]
subst_tt_many_id_on_fresh [in GMuAnnot.InfrastructureSubst]
subst_tb_id_on_fresh [in GMuAnnot.InfrastructureSubst]
subst_te_many_commutes_open [in GMuAnnot.InfrastructureSubst]
subst_tt_many_free [in GMuAnnot.InfrastructureSubst]
subst_te_intro_many [in GMuAnnot.InfrastructureSubst]
subst_intro_commutes_opens_te [in GMuAnnot.InfrastructureSubst]
subst_commutes_with_unrelated_opens_te [in GMuAnnot.InfrastructureSubst]
subst_commutes_open_tt_many [in GMuAnnot.InfrastructureSubst]
subst_removes_var [in GMuAnnot.InfrastructureSubst]
subst_idempotent_through_many_open [in GMuAnnot.InfrastructureSubst]
subst_idempotent [in GMuAnnot.InfrastructureSubst]
subst_ee_value [in GMuAnnot.InfrastructureSubst]
subst_ee_term [in GMuAnnot.InfrastructureSubst]
subst_te_value [in GMuAnnot.InfrastructureSubst]
subst_te_term [in GMuAnnot.InfrastructureSubst]
subst_commutes_with_unrelated_opens_te_ee [in GMuAnnot.InfrastructureSubst]
subst_commutes_with_unrelated_opens_te_te [in GMuAnnot.InfrastructureSubst]
subst_tt_type [in GMuAnnot.InfrastructureSubst]
subst_map_reverse_type [in GMuAnnot.InfrastructureSubst]
subst_ee_open_te_var [in GMuAnnot.InfrastructureSubst]
subst_te_open_ee_var [in GMuAnnot.InfrastructureSubst]
subst_ee_intro [in GMuAnnot.InfrastructureSubst]
subst_ee_open_ee_var [in GMuAnnot.InfrastructureSubst]
subst_ee_open_ee [in GMuAnnot.InfrastructureSubst]
subst_ee_fresh [in GMuAnnot.InfrastructureSubst]
subst_te_intro [in GMuAnnot.InfrastructureSubst]
subst_te_open_te_var [in GMuAnnot.InfrastructureSubst]
subst_te_open_te [in GMuAnnot.InfrastructureSubst]
subst_te_fresh [in GMuAnnot.InfrastructureSubst]
subst_tt_intro_many [in GMuAnnot.InfrastructureSubst]
subst_intro_commutes_opens [in GMuAnnot.InfrastructureSubst]
subst_commutes_with_unrelated_opens [in GMuAnnot.InfrastructureSubst]
subst_tt_intro [in GMuAnnot.InfrastructureSubst]
subst_tt_open_tt_var [in GMuAnnot.InfrastructureSubst]
subst_tt_open_tt [in GMuAnnot.InfrastructureSubst]
subst_tt_open_tt_rec [in GMuAnnot.InfrastructureSubst]
subst_tt_fresh [in GMuAnnot.InfrastructureSubst]
subst_td_alphas [in GMuAnnot.InfrastructureFV]
subst_src_app [in GMuAnnot.InfrastructureFV]
subst_match_notin_srcs2 [in GMuAnnot.InfrastructureFV]
subst_td_eqs [in GMuAnnot.Regularity2]
subst_ttprim_open_tt [in GMuAnnot.InfrastructureSubstPrim]
subst_tt_prime_reduce_typ_unit [in GMuAnnot.InfrastructureSubstPrim]
subst_tt_prime_reduce_typ_gadt [in GMuAnnot.InfrastructureSubstPrim]
subst_tt_prime_reduce_arrow [in GMuAnnot.InfrastructureSubstPrim]
subst_tt_prime_reduce_tuple [in GMuAnnot.InfrastructureSubstPrim]
subst_tt_prime_reduce_typ_all [in GMuAnnot.InfrastructureSubstPrim]
subst_tt_inside [in GMuAnnot.InfrastructureSubstPrim]
subst_ttΘ_fresh [in GMuAnnot.InfrastructureSubstPrim]
subst_tb_many_split [in GMuAnnot.Prelude]
subst_strengthen_true_eq [in GMuAnnot.SubstMatch]
subst_match_inv_missing_var [in GMuAnnot.SubstMatch]
subst_eq_weaken2 [in GMuAnnot.SubstMatch]
subst_match_split [in GMuAnnot.SubstMatch]
subst_remove_used_var [in GMuAnnot.SubstMatch]
subst_eq_reorder2 [in GMuAnnot.SubstMatch]
subst_eq_reorder2_2 [in GMuAnnot.SubstMatch]
subst_eq_reorder1 [in GMuAnnot.SubstMatch]
subst_tt_split [in GMuAnnot.SubstMatch]
subst_eq_reorder1_2 [in GMuAnnot.SubstMatch]
subst_idempotent_simple [in GMuAnnot.SubstMatch]
subst_has_closed [in GMuAnnot.SubstMatch]
subst_has_wft [in GMuAnnot.SubstMatch]
subst_tt_prime_reduce_typ_fvar_undefined [in GMuAnnot.SubstMatch]
subst_tt_prime_reduce_typ_fvar_defined [in GMuAnnot.SubstMatch]
subst_match_remove_right_var3 [in GMuAnnot.SubstMatch]
subst_match_remove_unused_var [in GMuAnnot.SubstMatch]
subst_eq_weaken [in GMuAnnot.SubstMatch]
subst_eq_strengthen_gen [in GMuAnnot.SubstMatch]
subst_eq_strengthen [in GMuAnnot.SubstMatch]
subst_match_remove_right_var2 [in GMuAnnot.SubstMatch]
subst_match_remove_right_var [in GMuAnnot.SubstMatch]
subst_match_notin_srcs [in GMuAnnot.SubstMatch]
subst_match_decompose_var [in GMuAnnot.SubstMatch]
subst_match_remove_eq [in GMuAnnot.SubstMatch]
subst_sources_from_match [in GMuAnnot.SubstMatch]
T
teq_axiom [in GMuAnnot.Equations]teq_transitivity [in GMuAnnot.Equations]
teq_symmetry [in GMuAnnot.Equations]
teq_reflexivity [in GMuAnnot.Equations]
teq_open [in GMuAnnot.SubstMatch]
term_te_closed [in GMuAnnot.InfrastructureOpen]
te_closed_id [in GMuAnnot.InfrastructureOpen]
te_opening_te_many_adds [in GMuAnnot.InfrastructureOpen]
te_opening_ee_preserves [in GMuAnnot.InfrastructureOpen]
te_opening_te_adds_one [in GMuAnnot.InfrastructureOpen]
Tgen_from_any [in GMuAnnot.Regularity]
type_from_wft [in GMuAnnot.Regularity]
type_closed [in GMuAnnot.InfrastructureOpen]
typing_exfalso [in GMuAnnot.Equations]
typing_replace_typ [in GMuAnnot.Preservation]
typing_replace_typ_gen [in GMuAnnot.Preservation]
typing_through_subst_te_many [in GMuAnnot.Preservation]
typing_through_subst_te_3 [in GMuAnnot.Preservation]
typing_through_subst_te_gen [in GMuAnnot.Preservation]
typing_through_subst_ee_fix [in GMuAnnot.Preservation]
typing_through_subst_ee_lam [in GMuAnnot.Preservation]
typing_weakening [in GMuAnnot.Preservation]
typing_weakening_delta_many [in GMuAnnot.Preservation]
typing_weakening_delta_many_eq [in GMuAnnot.Preservation]
typing_weakening_delta [in GMuAnnot.Preservation]
typing_weakening_delta_eq [in GMuAnnot.Preservation]
typing_implies_term [in GMuAnnot.Regularity]
typing_regular [in GMuAnnot.Regularity]
U
union_empty [in GMuAnnot.Prelude]union_distributes [in GMuAnnot.Prelude]
union_fold_detach [in GMuAnnot.Prelude]
union_distribute [in GMuAnnot.Prelude]
V
value_regular [in GMuAnnot.Prelude]value_is_term [in GMuAnnot.Prelude]
W
wft_open_many [in GMuAnnot.Regularity]wft_subst_tb_many [in GMuAnnot.Regularity]
wft_open [in GMuAnnot.Regularity]
wft_subst_tb [in GMuAnnot.Regularity]
wft_weaken [in GMuAnnot.Regularity]
wft_type [in GMuAnnot.Regularity]
wft_strengthen_typ_many [in GMuAnnot.Regularity]
wft_strengthen_equations [in GMuAnnot.Regularity]
wft_strengthen_equation [in GMuAnnot.Regularity]
wft_strengthen_typ [in GMuAnnot.Regularity]
wft_from_env_has_typ [in GMuAnnot.Regularity]
wft_gives_fv [in GMuAnnot.InfrastructureFV]
wft_subst_tb_3 [in GMuAnnot.Regularity2]
wft_subst_tb_2 [in GMuAnnot.Regularity2]
wft_weaken_simple [in GMuAnnot.Regularity2]
wft_subst_matching [in GMuAnnot.SubstMatch]
wft_subst_matching_gen [in GMuAnnot.SubstMatch]
Inductive Index
C
Clause [in GMuAnnot.Definitions]R
red [in GMuAnnot.Definitions]T
term [in GMuAnnot.Definitions]te_closed_in_surroundings [in GMuAnnot.InfrastructureOpen]
trm [in GMuAnnot.Definitions]
typing [in GMuAnnot.Definitions]
typ_closed_in_surroundings [in GMuAnnot.InfrastructureOpen]
V
value [in GMuAnnot.Definitions]Section Index
M
ManyTest [in GMuAnnot.DefinitionsTests]S
SimpleEquationProperties [in GMuAnnot.Equations]T
trm_ind' [in GMuAnnot.Definitions]Definition Index
C
clauseArity [in GMuAnnot.Definitions]clauseTerm [in GMuAnnot.Definitions]
F
fv_trm [in GMuAnnot.Definitions]M
map_clause_trm_trm [in GMuAnnot.Definitions]map_clause_trms [in GMuAnnot.Definitions]
O
open_te_many_var [in GMuAnnot.Definitions]open_te_many [in GMuAnnot.Definitions]
open_ee [in GMuAnnot.Definitions]
open_te [in GMuAnnot.Definitions]
open_ee_rec [in GMuAnnot.Definitions]
open_te_rec [in GMuAnnot.Definitions]
P
preservation [in GMuAnnot.Definitions]progress [in GMuAnnot.Definitions]
S
subst_ee [in GMuAnnot.Definitions]subst_te [in GMuAnnot.Definitions]
subst_te_many [in GMuAnnot.InfrastructureSubst]
sum [in GMuAnnot.Definitions]
T
trm_size [in GMuAnnot.Definitions]trm_ind' [in GMuAnnot.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 | (2362 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 | (27 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 | (1910 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 | (17 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 | (16 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 | (86 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 | (276 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 | (8 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 | (3 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 | (19 entries) |