| 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 | (2458 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 | (47 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 | (1882 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| 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 | (45 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 | (133 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (26 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 | (37 entries) |
| Instance 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 | (145 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 | (7 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (31 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 | (87 entries) |
Global Index
A
ab:303 [binder, in coqrel.RelOperators]acc [projection, in coqrel.KLR]
acc:211 [binder, in coqrel.LogicalRelationsTests]
acc:419 [binder, in coqrel.RelOperators]
acc:428 [binder, in coqrel.RelOperators]
acc:432 [binder, in coqrel.RelOperators]
acc:441 [binder, in coqrel.RelOperators]
after:321 [binder, in coqrel.RelOperators]
all_monotonic_params [instance, in coqrel.Relators]
all_monotonic [instance, in coqrel.Relators]
andb_leb [instance, in coqrel.BoolRel]
and_monotonic [instance, in coqrel.Relators]
apply_candidate_subrel [instance, in coqrel.Monotonicity]
apply_candidate [instance, in coqrel.Monotonicity]
app_rel [instance, in coqrel.Relators]
arrow_pointwise_rel_compose [instance, in coqrel.Relators]
arrow_pointwise_refl [lemma, in coqrel.Relators]
arrow_pointwise_relim [lemma, in coqrel.Relators]
arrow_pointwise_rintro [lemma, in coqrel.Relators]
arrow_pointwise_subrel_params [instance, in coqrel.Relators]
arrow_pointwise_subrel [instance, in coqrel.Relators]
arrow_pointwise_rel [definition, in coqrel.Relators]
arrow_rdecompose [instance, in coqrel.RelClasses]
arrow_rcompose [instance, in coqrel.RelClasses]
ARROW_REL_COMPOSE [section, in coqrel.RelClasses]
arrow_corefl [instance, in coqrel.RelClasses]
arrow_refl [instance, in coqrel.RelClasses]
ARROW_MOD [section, in coqrel.KLR]
arrow_pointwise_klr [definition, in coqrel.KLR]
arrow_klr [definition, in coqrel.KLR]
arrow_relim [lemma, in coqrel.RelDefinitions]
arrow_rintro [lemma, in coqrel.RelDefinitions]
arrow_subrel_params [instance, in coqrel.RelDefinitions]
arrow_subrel [instance, in coqrel.RelDefinitions]
arrow_rel [definition, in coqrel.RelDefinitions]
as_is_candidate [instance, in coqrel.Monotonicity]
A':201 [binder, in coqrel.RelOperators]
A':210 [binder, in coqrel.RelOperators]
A':236 [binder, in coqrel.RelOperators]
A':245 [binder, in coqrel.RelOperators]
A1:1 [binder, in coqrel.OptionRel]
A1:10 [binder, in coqrel.Transport]
A1:102 [binder, in coqrel.KLR]
A1:106 [binder, in coqrel.KLR]
A1:119 [binder, in coqrel.RelDefinitions]
A1:129 [binder, in coqrel.RelDefinitions]
a1:130 [binder, in coqrel.LogicalRelationsTests]
A1:131 [binder, in coqrel.KLR]
A1:133 [binder, in coqrel.RelDefinitions]
A1:134 [binder, in coqrel.LogicalRelationsTests]
A1:143 [binder, in coqrel.RelDefinitions]
A1:149 [binder, in coqrel.Relators]
A1:149 [binder, in coqrel.LogicalRelationsTests]
A1:161 [binder, in coqrel.Relators]
a1:18 [binder, in coqrel.Transport]
A1:18 [binder, in coqrel.RelDefinitions]
A1:181 [binder, in coqrel.LogicalRelationsTests]
A1:185 [binder, in coqrel.Relators]
a1:19 [binder, in coqrel.KLR]
A1:199 [binder, in coqrel.Relators]
A1:203 [binder, in coqrel.Relators]
a1:210 [binder, in coqrel.Relators]
A1:222 [binder, in coqrel.RelOperators]
A1:234 [binder, in coqrel.Relators]
A1:239 [binder, in coqrel.Relators]
A1:243 [binder, in coqrel.Relators]
A1:254 [binder, in coqrel.RelOperators]
A1:257 [binder, in coqrel.Relators]
A1:26 [binder, in coqrel.OptionRel]
A1:264 [binder, in coqrel.Relators]
A1:265 [binder, in coqrel.RelOperators]
A1:27 [binder, in coqrel.KLR]
A1:275 [binder, in coqrel.RelOperators]
A1:284 [binder, in coqrel.RelOperators]
A1:29 [binder, in coqrel.Transport]
A1:305 [binder, in coqrel.RelOperators]
A1:312 [binder, in coqrel.RelOperators]
A1:324 [binder, in coqrel.RelOperators]
A1:34 [binder, in coqrel.OptionRel]
a1:36 [binder, in coqrel.Transport]
A1:36 [binder, in coqrel.LogicalRelationsTests]
A1:40 [binder, in coqrel.Transport]
A1:45 [binder, in coqrel.RelClasses]
a1:49 [binder, in coqrel.Transport]
A1:9 [binder, in coqrel.OptionRel]
A1:9 [binder, in coqrel.KLR]
A1:91 [binder, in coqrel.KLR]
A1:98 [binder, in coqrel.KLR]
A2:10 [binder, in coqrel.OptionRel]
A2:10 [binder, in coqrel.KLR]
A2:103 [binder, in coqrel.KLR]
A2:107 [binder, in coqrel.KLR]
A2:12 [binder, in coqrel.Transport]
A2:120 [binder, in coqrel.RelDefinitions]
A2:130 [binder, in coqrel.RelDefinitions]
a2:131 [binder, in coqrel.LogicalRelationsTests]
A2:134 [binder, in coqrel.KLR]
A2:134 [binder, in coqrel.RelDefinitions]
A2:135 [binder, in coqrel.LogicalRelationsTests]
A2:144 [binder, in coqrel.RelDefinitions]
A2:150 [binder, in coqrel.Relators]
A2:150 [binder, in coqrel.LogicalRelationsTests]
A2:162 [binder, in coqrel.Relators]
A2:182 [binder, in coqrel.LogicalRelationsTests]
A2:186 [binder, in coqrel.Relators]
a2:19 [binder, in coqrel.Transport]
A2:19 [binder, in coqrel.RelDefinitions]
A2:2 [binder, in coqrel.OptionRel]
a2:20 [binder, in coqrel.KLR]
A2:200 [binder, in coqrel.Relators]
A2:205 [binder, in coqrel.Relators]
a2:211 [binder, in coqrel.Relators]
A2:223 [binder, in coqrel.RelOperators]
A2:235 [binder, in coqrel.Relators]
A2:240 [binder, in coqrel.Relators]
A2:244 [binder, in coqrel.Relators]
A2:255 [binder, in coqrel.RelOperators]
A2:258 [binder, in coqrel.Relators]
A2:265 [binder, in coqrel.Relators]
A2:266 [binder, in coqrel.RelOperators]
A2:27 [binder, in coqrel.OptionRel]
A2:276 [binder, in coqrel.RelOperators]
A2:285 [binder, in coqrel.RelOperators]
A2:29 [binder, in coqrel.KLR]
A2:30 [binder, in coqrel.Transport]
A2:308 [binder, in coqrel.RelOperators]
A2:315 [binder, in coqrel.RelOperators]
A2:327 [binder, in coqrel.RelOperators]
A2:35 [binder, in coqrel.OptionRel]
a2:37 [binder, in coqrel.Transport]
A2:37 [binder, in coqrel.LogicalRelationsTests]
A2:41 [binder, in coqrel.Transport]
A2:46 [binder, in coqrel.RelClasses]
a2:50 [binder, in coqrel.Transport]
A2:92 [binder, in coqrel.KLR]
A2:99 [binder, in coqrel.KLR]
A3:224 [binder, in coqrel.RelOperators]
A3:42 [binder, in coqrel.Transport]
A3:47 [binder, in coqrel.RelClasses]
a3:51 [binder, in coqrel.Transport]
A:1 [binder, in coqrel.Transport]
A:1 [binder, in coqrel.PreOrderTactic]
A:1 [binder, in coqrel.Relators]
A:1 [binder, in coqrel.RelClasses]
A:1 [binder, in coqrel.RelDefinitions]
A:1 [binder, in coqrel.RelOperators]
A:1 [binder, in coqrel.RelQuotient]
A:1 [binder, in coqrel.Monotonicity]
A:1 [binder, in coqrel.MorphismsInterop]
A:10 [binder, in coqrel.RelClasses]
A:10 [binder, in coqrel.RDestruct]
A:10 [binder, in coqrel.RelDefinitions]
a:10 [binder, in coqrel.RelQuotient]
A:101 [binder, in coqrel.LogicalRelationsTests]
A:102 [binder, in coqrel.Monotonicity]
A:103 [binder, in coqrel.RelOperators]
A:105 [binder, in coqrel.RelDefinitions]
A:105 [binder, in coqrel.RelOperators]
A:107 [binder, in coqrel.RelDefinitions]
A:107 [binder, in coqrel.LogicalRelationsTests]
A:108 [binder, in coqrel.KLR]
A:109 [binder, in coqrel.Relators]
A:109 [binder, in coqrel.RelDefinitions]
A:11 [binder, in coqrel.Relators]
A:11 [binder, in coqrel.MorphismsInterop]
A:111 [binder, in coqrel.RelOperators]
A:111 [binder, in coqrel.LogicalRelationsTests]
A:112 [binder, in coqrel.Monotonicity]
a:114 [binder, in coqrel.Relators]
a:114 [binder, in coqrel.KLR]
A:115 [binder, in coqrel.LogicalRelationsTests]
A:116 [binder, in coqrel.Relators]
A:116 [binder, in coqrel.KLR]
A:117 [binder, in coqrel.RelOperators]
A:118 [binder, in coqrel.Relators]
A:118 [binder, in coqrel.LogicalRelationsTests]
A:12 [binder, in coqrel.OptionRel]
A:12 [binder, in coqrel.RelQuotient]
A:120 [binder, in coqrel.Monotonicity]
A:121 [binder, in coqrel.RelOperators]
A:122 [binder, in coqrel.LogicalRelationsTests]
a:123 [binder, in coqrel.KLR]
A:125 [binder, in coqrel.KLR]
A:125 [binder, in coqrel.RelOperators]
A:125 [binder, in coqrel.LogicalRelationsTests]
A:127 [binder, in coqrel.Relators]
A:128 [binder, in coqrel.KLR]
A:128 [binder, in coqrel.RelOperators]
A:130 [binder, in coqrel.Monotonicity]
a:133 [binder, in coqrel.Relators]
A:133 [binder, in coqrel.RelOperators]
A:134 [binder, in coqrel.Relators]
A:136 [binder, in coqrel.Relators]
A:137 [binder, in coqrel.RelOperators]
A:14 [binder, in coqrel.LogicalRelationsTests]
A:140 [binder, in coqrel.KLR]
A:141 [binder, in coqrel.RelOperators]
A:142 [binder, in coqrel.RelOperators]
A:142 [binder, in coqrel.Monotonicity]
A:143 [binder, in coqrel.LogicalRelationsTests]
A:144 [binder, in coqrel.RelOperators]
A:146 [binder, in coqrel.RelOperators]
A:148 [binder, in coqrel.KLR]
A:148 [binder, in coqrel.RelOperators]
A:149 [binder, in coqrel.Monotonicity]
A:15 [binder, in coqrel.RelOperators]
A:15 [binder, in coqrel.Monotonicity]
a:15 [binder, in coqrel.LogicalRelationsTests]
A:150 [binder, in coqrel.KLR]
A:156 [binder, in coqrel.RelOperators]
A:156 [binder, in coqrel.Monotonicity]
A:159 [binder, in coqrel.KLR]
A:159 [binder, in coqrel.RelOperators]
A:16 [binder, in coqrel.OptionRel]
A:161 [binder, in coqrel.LogicalRelationsTests]
A:162 [binder, in coqrel.RelOperators]
A:165 [binder, in coqrel.Relators]
A:165 [binder, in coqrel.RelOperators]
A:168 [binder, in coqrel.RelOperators]
A:169 [binder, in coqrel.Relators]
A:169 [binder, in coqrel.KLR]
A:17 [binder, in coqrel.RelQuotient]
A:173 [binder, in coqrel.Relators]
A:175 [binder, in coqrel.RelOperators]
A:177 [binder, in coqrel.Relators]
A:177 [binder, in coqrel.KLR]
A:179 [binder, in coqrel.KLR]
A:18 [binder, in coqrel.OptionRel]
A:18 [binder, in coqrel.Relators]
A:180 [binder, in coqrel.RelOperators]
A:181 [binder, in coqrel.Relators]
A:187 [binder, in coqrel.KLR]
A:19 [binder, in coqrel.RDestruct]
A:19 [binder, in coqrel.RelQuotient]
A:193 [binder, in coqrel.LogicalRelationsTests]
A:199 [binder, in coqrel.RelOperators]
A:2 [binder, in coqrel.KLR]
A:20 [binder, in coqrel.OptionRel]
A:20 [binder, in coqrel.LogicalRelationsTests]
A:201 [binder, in coqrel.KLR]
A:204 [binder, in coqrel.RelDefinitions]
A:204 [binder, in coqrel.LogicalRelationsTests]
A:206 [binder, in coqrel.RelDefinitions]
A:208 [binder, in coqrel.RelOperators]
A:21 [binder, in coqrel.RelClasses]
A:21 [binder, in coqrel.RelOperators]
A:21 [binder, in coqrel.RelQuotient]
A:21 [binder, in coqrel.MorphismsInterop]
A:210 [binder, in coqrel.KLR]
A:211 [binder, in coqrel.RelDefinitions]
A:212 [binder, in coqrel.LogicalRelationsTests]
A:214 [binder, in coqrel.Relators]
a:214 [binder, in coqrel.KLR]
A:214 [binder, in coqrel.RelOperators]
A:218 [binder, in coqrel.Relators]
A:218 [binder, in coqrel.RelDefinitions]
A:218 [binder, in coqrel.RelOperators]
A:22 [binder, in coqrel.Transport]
A:22 [binder, in coqrel.OptionRel]
a:220 [binder, in coqrel.LogicalRelationsTests]
A:222 [binder, in coqrel.Relators]
A:223 [binder, in coqrel.RelDefinitions]
A:224 [binder, in coqrel.KLR]
A:226 [binder, in coqrel.Relators]
A:227 [binder, in coqrel.RelDefinitions]
A:227 [binder, in coqrel.LogicalRelationsTests]
A:23 [binder, in coqrel.MorphismsInterop]
A:230 [binder, in coqrel.Relators]
A:230 [binder, in coqrel.KLR]
A:232 [binder, in coqrel.KLR]
A:232 [binder, in coqrel.RelDefinitions]
A:234 [binder, in coqrel.RelOperators]
A:235 [binder, in coqrel.LogicalRelationsTests]
A:238 [binder, in coqrel.KLR]
a:24 [binder, in coqrel.RelQuotient]
A:241 [binder, in coqrel.LogicalRelationsTests]
A:243 [binder, in coqrel.RelOperators]
A:248 [binder, in coqrel.KLR]
A:248 [binder, in coqrel.LogicalRelationsTests]
a:25 [binder, in coqrel.MorphismsInterop]
A:250 [binder, in coqrel.Relators]
a:250 [binder, in coqrel.LogicalRelationsTests]
a:251 [binder, in coqrel.LogicalRelationsTests]
A:252 [binder, in coqrel.LogicalRelationsTests]
a:254 [binder, in coqrel.LogicalRelationsTests]
a:255 [binder, in coqrel.Relators]
A:255 [binder, in coqrel.KLR]
A:255 [binder, in coqrel.LogicalRelationsTests]
A:257 [binder, in coqrel.LogicalRelationsTests]
A:26 [binder, in coqrel.RelClasses]
A:26 [binder, in coqrel.RDestruct]
A:26 [binder, in coqrel.RelOperators]
A:261 [binder, in coqrel.KLR]
a:27 [binder, in coqrel.Transport]
A:270 [binder, in coqrel.KLR]
A:271 [binder, in coqrel.RelOperators]
A:28 [binder, in coqrel.Monotonicity]
A:28 [binder, in coqrel.LogicalRelationsTests]
A:286 [binder, in coqrel.Relators]
A:288 [binder, in coqrel.Relators]
A:289 [binder, in coqrel.Relators]
a:29 [binder, in coqrel.LogicalRelationsTests]
a:29 [binder, in coqrel.MorphismsInterop]
A:293 [binder, in coqrel.RelOperators]
a:297 [binder, in coqrel.RelOperators]
A:299 [binder, in coqrel.RelOperators]
A:3 [binder, in coqrel.RDestruct]
A:3 [binder, in coqrel.LogicalRelationsTests]
A:3 [binder, in coqrel.MorphismsInterop]
A:30 [binder, in coqrel.MorphismsInterop]
A:31 [binder, in coqrel.KLR]
A:31 [binder, in coqrel.RelOperators]
A:319 [binder, in coqrel.RelOperators]
A:32 [binder, in coqrel.RelDefinitions]
a:32 [binder, in coqrel.MorphismsInterop]
A:336 [binder, in coqrel.RelOperators]
a:337 [binder, in coqrel.RelOperators]
A:340 [binder, in coqrel.RelOperators]
a:341 [binder, in coqrel.RelOperators]
A:342 [binder, in coqrel.RelOperators]
a:343 [binder, in coqrel.RelOperators]
A:344 [binder, in coqrel.RelOperators]
A:349 [binder, in coqrel.RelOperators]
A:35 [binder, in coqrel.RelDefinitions]
A:351 [binder, in coqrel.RelOperators]
A:356 [binder, in coqrel.RelOperators]
A:358 [binder, in coqrel.RelOperators]
A:36 [binder, in coqrel.RelOperators]
a:36 [binder, in coqrel.MorphismsInterop]
A:363 [binder, in coqrel.RelOperators]
A:364 [binder, in coqrel.RelOperators]
A:366 [binder, in coqrel.RelOperators]
A:37 [binder, in coqrel.OptionRel]
A:37 [binder, in coqrel.RelClasses]
A:375 [binder, in coqrel.RelOperators]
A:38 [binder, in coqrel.Monotonicity]
A:382 [binder, in coqrel.RelOperators]
A:39 [binder, in coqrel.RelOperators]
A:39 [binder, in coqrel.MorphismsInterop]
A:391 [binder, in coqrel.RelOperators]
a:4 [binder, in coqrel.Transport]
a:4 [binder, in coqrel.PreOrderTactic]
A:4 [binder, in coqrel.RelDefinitions]
a:4 [binder, in coqrel.LogicalRelationsTests]
A:400 [binder, in coqrel.RelOperators]
A:407 [binder, in coqrel.RelOperators]
A:41 [binder, in coqrel.OptionRel]
A:41 [binder, in coqrel.RelClasses]
A:41 [binder, in coqrel.MorphismsInterop]
A:417 [binder, in coqrel.RelOperators]
A:42 [binder, in coqrel.RelOperators]
a:422 [binder, in coqrel.RelOperators]
A:426 [binder, in coqrel.RelOperators]
A:43 [binder, in coqrel.OptionRel]
A:430 [binder, in coqrel.RelOperators]
A:439 [binder, in coqrel.RelOperators]
A:44 [binder, in coqrel.LogicalRelationsTests]
A:45 [binder, in coqrel.OptionRel]
A:45 [binder, in coqrel.RelOperators]
a:46 [binder, in coqrel.MorphismsInterop]
A:47 [binder, in coqrel.OptionRel]
A:47 [binder, in coqrel.Monotonicity]
A:47 [binder, in coqrel.MorphismsInterop]
A:48 [binder, in coqrel.RelOperators]
a:5 [binder, in coqrel.RelQuotient]
A:5 [binder, in coqrel.LogicalRelationsTests]
A:50 [binder, in coqrel.RelDefinitions]
A:51 [binder, in coqrel.OptionRel]
A:52 [binder, in coqrel.LogicalRelationsTests]
a:52 [binder, in coqrel.MorphismsInterop]
A:54 [binder, in coqrel.RelOperators]
A:55 [binder, in coqrel.Monotonicity]
A:55 [binder, in coqrel.MorphismsInterop]
a:56 [binder, in coqrel.OptionRel]
A:56 [binder, in coqrel.RelOperators]
A:57 [binder, in coqrel.MorphismsInterop]
A:58 [binder, in coqrel.OptionRel]
A:58 [binder, in coqrel.RelDefinitions]
A:59 [binder, in coqrel.LogicalRelationsTests]
a:59 [binder, in coqrel.MorphismsInterop]
A:6 [binder, in coqrel.PreOrderTactic]
a:6 [binder, in coqrel.RelDefinitions]
a:6 [binder, in coqrel.LogicalRelationsTests]
A:60 [binder, in coqrel.MorphismsInterop]
A:61 [binder, in coqrel.Monotonicity]
A:62 [binder, in coqrel.RelOperators]
A:64 [binder, in coqrel.RelDefinitions]
A:66 [binder, in coqrel.LogicalRelationsTests]
A:67 [binder, in coqrel.RelOperators]
a:7 [binder, in coqrel.Relators]
A:7 [binder, in coqrel.RelClasses]
A:7 [binder, in coqrel.RelOperators]
A:7 [binder, in coqrel.Monotonicity]
A:72 [binder, in coqrel.RelOperators]
A:72 [binder, in coqrel.Monotonicity]
A:73 [binder, in coqrel.RelDefinitions]
a:73 [binder, in coqrel.LogicalRelationsTests]
a:75 [binder, in coqrel.LogicalRelationsTests]
A:77 [binder, in coqrel.RelOperators]
A:77 [binder, in coqrel.LogicalRelationsTests]
A:78 [binder, in coqrel.RelDefinitions]
A:8 [binder, in coqrel.Relators]
A:8 [binder, in coqrel.RelClasses]
A:8 [binder, in coqrel.RelQuotient]
A:8 [binder, in coqrel.LogicalRelationsTests]
A:80 [binder, in coqrel.RelOperators]
A:82 [binder, in coqrel.Monotonicity]
A:83 [binder, in coqrel.RelOperators]
A:85 [binder, in coqrel.LogicalRelationsTests]
A:86 [binder, in coqrel.RelOperators]
A:87 [binder, in coqrel.RelDefinitions]
A:89 [binder, in coqrel.RelOperators]
A:9 [binder, in coqrel.RelOperators]
a:9 [binder, in coqrel.LogicalRelationsTests]
A:90 [binder, in coqrel.LogicalRelationsTests]
A:91 [binder, in coqrel.Monotonicity]
A:92 [binder, in coqrel.RelOperators]
A:94 [binder, in coqrel.RelDefinitions]
A:94 [binder, in coqrel.RelOperators]
A:95 [binder, in coqrel.KLR]
A:96 [binder, in coqrel.Monotonicity]
A:97 [binder, in coqrel.RelOperators]
A:99 [binder, in coqrel.RelDefinitions]
B
before:320 [binder, in coqrel.RelOperators]BoolRel [library]
B':202 [binder, in coqrel.RelOperators]
B':211 [binder, in coqrel.RelOperators]
B':237 [binder, in coqrel.RelOperators]
B':246 [binder, in coqrel.RelOperators]
B1:100 [binder, in coqrel.KLR]
B1:104 [binder, in coqrel.KLR]
B1:11 [binder, in coqrel.Transport]
B1:12 [binder, in coqrel.Relators]
B1:12 [binder, in coqrel.KLR]
B1:121 [binder, in coqrel.RelDefinitions]
B1:131 [binder, in coqrel.RelDefinitions]
B1:132 [binder, in coqrel.KLR]
B1:135 [binder, in coqrel.RelDefinitions]
B1:136 [binder, in coqrel.LogicalRelationsTests]
B1:145 [binder, in coqrel.RelDefinitions]
B1:151 [binder, in coqrel.Relators]
B1:151 [binder, in coqrel.LogicalRelationsTests]
B1:163 [binder, in coqrel.Relators]
b1:17 [binder, in coqrel.BoolRel]
B1:183 [binder, in coqrel.LogicalRelationsTests]
B1:187 [binder, in coqrel.Relators]
B1:19 [binder, in coqrel.Relators]
B1:2 [binder, in coqrel.Relators]
b1:20 [binder, in coqrel.Transport]
B1:201 [binder, in coqrel.Relators]
B1:204 [binder, in coqrel.Relators]
b1:212 [binder, in coqrel.Relators]
b1:22 [binder, in coqrel.KLR]
B1:225 [binder, in coqrel.RelOperators]
B1:256 [binder, in coqrel.RelOperators]
B1:267 [binder, in coqrel.RelOperators]
B1:277 [binder, in coqrel.RelOperators]
B1:28 [binder, in coqrel.KLR]
B1:286 [binder, in coqrel.RelOperators]
B1:306 [binder, in coqrel.RelOperators]
B1:31 [binder, in coqrel.Transport]
B1:313 [binder, in coqrel.RelOperators]
B1:325 [binder, in coqrel.RelOperators]
b1:38 [binder, in coqrel.Transport]
B1:38 [binder, in coqrel.LogicalRelationsTests]
B1:43 [binder, in coqrel.Transport]
B1:51 [binder, in coqrel.RelClasses]
b1:52 [binder, in coqrel.Transport]
B1:9 [binder, in coqrel.Relators]
B1:93 [binder, in coqrel.KLR]
B1:96 [binder, in coqrel.KLR]
B2:10 [binder, in coqrel.Relators]
B2:101 [binder, in coqrel.KLR]
B2:105 [binder, in coqrel.KLR]
B2:122 [binder, in coqrel.RelDefinitions]
B2:13 [binder, in coqrel.Transport]
B2:13 [binder, in coqrel.Relators]
B2:13 [binder, in coqrel.KLR]
B2:132 [binder, in coqrel.RelDefinitions]
B2:135 [binder, in coqrel.KLR]
B2:136 [binder, in coqrel.RelDefinitions]
B2:137 [binder, in coqrel.LogicalRelationsTests]
B2:146 [binder, in coqrel.RelDefinitions]
B2:152 [binder, in coqrel.Relators]
B2:152 [binder, in coqrel.LogicalRelationsTests]
B2:164 [binder, in coqrel.Relators]
B2:184 [binder, in coqrel.LogicalRelationsTests]
B2:188 [binder, in coqrel.Relators]
B2:20 [binder, in coqrel.Relators]
b2:20 [binder, in coqrel.BoolRel]
B2:202 [binder, in coqrel.Relators]
B2:206 [binder, in coqrel.Relators]
b2:21 [binder, in coqrel.Transport]
b2:213 [binder, in coqrel.Relators]
B2:226 [binder, in coqrel.RelOperators]
b2:23 [binder, in coqrel.KLR]
B2:257 [binder, in coqrel.RelOperators]
B2:268 [binder, in coqrel.RelOperators]
B2:278 [binder, in coqrel.RelOperators]
B2:287 [binder, in coqrel.RelOperators]
B2:3 [binder, in coqrel.Relators]
B2:30 [binder, in coqrel.KLR]
B2:309 [binder, in coqrel.RelOperators]
B2:316 [binder, in coqrel.RelOperators]
B2:32 [binder, in coqrel.Transport]
B2:328 [binder, in coqrel.RelOperators]
b2:39 [binder, in coqrel.Transport]
B2:39 [binder, in coqrel.LogicalRelationsTests]
B2:44 [binder, in coqrel.Transport]
B2:52 [binder, in coqrel.RelClasses]
b2:53 [binder, in coqrel.Transport]
B2:94 [binder, in coqrel.KLR]
B2:97 [binder, in coqrel.KLR]
B3:227 [binder, in coqrel.RelOperators]
B3:45 [binder, in coqrel.Transport]
B3:53 [binder, in coqrel.RelClasses]
b3:54 [binder, in coqrel.Transport]
B:10 [binder, in coqrel.RelOperators]
b:10 [binder, in coqrel.LogicalRelationsTests]
B:100 [binder, in coqrel.RelDefinitions]
B:103 [binder, in coqrel.Monotonicity]
B:104 [binder, in coqrel.RelOperators]
B:106 [binder, in coqrel.RelDefinitions]
B:106 [binder, in coqrel.RelOperators]
B:109 [binder, in coqrel.KLR]
B:11 [binder, in coqrel.RelClasses]
B:11 [binder, in coqrel.RDestruct]
B:110 [binder, in coqrel.Relators]
B:110 [binder, in coqrel.RelDefinitions]
B:112 [binder, in coqrel.RelOperators]
B:113 [binder, in coqrel.Monotonicity]
b:115 [binder, in coqrel.Relators]
b:115 [binder, in coqrel.KLR]
B:117 [binder, in coqrel.Relators]
B:117 [binder, in coqrel.KLR]
B:118 [binder, in coqrel.RelOperators]
B:12 [binder, in coqrel.MorphismsInterop]
B:121 [binder, in coqrel.Monotonicity]
b:122 [binder, in coqrel.KLR]
B:122 [binder, in coqrel.RelOperators]
B:126 [binder, in coqrel.KLR]
B:126 [binder, in coqrel.RelOperators]
B:126 [binder, in coqrel.LogicalRelationsTests]
B:128 [binder, in coqrel.Relators]
B:129 [binder, in coqrel.KLR]
B:129 [binder, in coqrel.RelOperators]
B:13 [binder, in coqrel.OptionRel]
B:131 [binder, in coqrel.Monotonicity]
b:132 [binder, in coqrel.Relators]
b:132 [binder, in coqrel.LogicalRelationsTests]
B:134 [binder, in coqrel.RelOperators]
B:135 [binder, in coqrel.Relators]
B:138 [binder, in coqrel.RelOperators]
B:141 [binder, in coqrel.KLR]
B:143 [binder, in coqrel.RelOperators]
B:143 [binder, in coqrel.Monotonicity]
B:144 [binder, in coqrel.LogicalRelationsTests]
B:145 [binder, in coqrel.RelOperators]
B:147 [binder, in coqrel.RelOperators]
B:149 [binder, in coqrel.KLR]
B:149 [binder, in coqrel.RelOperators]
B:150 [binder, in coqrel.Monotonicity]
B:151 [binder, in coqrel.KLR]
B:157 [binder, in coqrel.RelOperators]
B:157 [binder, in coqrel.Monotonicity]
B:16 [binder, in coqrel.RelOperators]
B:16 [binder, in coqrel.Monotonicity]
b:16 [binder, in coqrel.LogicalRelationsTests]
B:160 [binder, in coqrel.KLR]
B:160 [binder, in coqrel.RelOperators]
B:162 [binder, in coqrel.LogicalRelationsTests]
B:163 [binder, in coqrel.RelOperators]
B:166 [binder, in coqrel.Relators]
B:166 [binder, in coqrel.RelOperators]
B:169 [binder, in coqrel.RelOperators]
B:17 [binder, in coqrel.OptionRel]
B:170 [binder, in coqrel.Relators]
B:170 [binder, in coqrel.KLR]
B:174 [binder, in coqrel.Relators]
B:176 [binder, in coqrel.RelOperators]
B:178 [binder, in coqrel.Relators]
B:178 [binder, in coqrel.KLR]
B:180 [binder, in coqrel.KLR]
B:181 [binder, in coqrel.RelOperators]
B:182 [binder, in coqrel.Relators]
B:188 [binder, in coqrel.KLR]
B:19 [binder, in coqrel.OptionRel]
B:2 [binder, in coqrel.Transport]
B:2 [binder, in coqrel.PreOrderTactic]
B:2 [binder, in coqrel.RelOperators]
B:2 [binder, in coqrel.Monotonicity]
B:2 [binder, in coqrel.MorphismsInterop]
B:20 [binder, in coqrel.RDestruct]
B:200 [binder, in coqrel.RelOperators]
B:202 [binder, in coqrel.KLR]
B:205 [binder, in coqrel.RelDefinitions]
B:205 [binder, in coqrel.LogicalRelationsTests]
B:207 [binder, in coqrel.RelDefinitions]
B:209 [binder, in coqrel.RelOperators]
B:21 [binder, in coqrel.LogicalRelationsTests]
B:211 [binder, in coqrel.KLR]
B:212 [binder, in coqrel.RelDefinitions]
B:213 [binder, in coqrel.LogicalRelationsTests]
B:215 [binder, in coqrel.Relators]
B:215 [binder, in coqrel.RelOperators]
b:217 [binder, in coqrel.KLR]
B:219 [binder, in coqrel.Relators]
B:219 [binder, in coqrel.RelDefinitions]
B:219 [binder, in coqrel.RelOperators]
B:22 [binder, in coqrel.RelOperators]
b:221 [binder, in coqrel.LogicalRelationsTests]
B:223 [binder, in coqrel.Relators]
B:224 [binder, in coqrel.RelDefinitions]
B:225 [binder, in coqrel.KLR]
B:227 [binder, in coqrel.Relators]
B:228 [binder, in coqrel.RelDefinitions]
B:228 [binder, in coqrel.LogicalRelationsTests]
B:23 [binder, in coqrel.Transport]
B:231 [binder, in coqrel.Relators]
B:231 [binder, in coqrel.KLR]
B:233 [binder, in coqrel.KLR]
B:233 [binder, in coqrel.RelDefinitions]
B:235 [binder, in coqrel.RelOperators]
B:236 [binder, in coqrel.LogicalRelationsTests]
B:239 [binder, in coqrel.KLR]
B:24 [binder, in coqrel.MorphismsInterop]
b:24 [binder, in coqrel.BoolRel]
B:242 [binder, in coqrel.LogicalRelationsTests]
B:244 [binder, in coqrel.RelOperators]
B:249 [binder, in coqrel.KLR]
b:25 [binder, in coqrel.BoolRel]
B:251 [binder, in coqrel.Relators]
b:256 [binder, in coqrel.Relators]
B:256 [binder, in coqrel.KLR]
B:262 [binder, in coqrel.KLR]
B:27 [binder, in coqrel.RelClasses]
B:27 [binder, in coqrel.RDestruct]
B:27 [binder, in coqrel.RelOperators]
B:271 [binder, in coqrel.KLR]
B:272 [binder, in coqrel.RelOperators]
b:28 [binder, in coqrel.Transport]
B:287 [binder, in coqrel.Relators]
B:29 [binder, in coqrel.Monotonicity]
B:294 [binder, in coqrel.RelOperators]
b:298 [binder, in coqrel.RelOperators]
B:3 [binder, in coqrel.KLR]
b:30 [binder, in coqrel.LogicalRelationsTests]
B:300 [binder, in coqrel.RelOperators]
B:31 [binder, in coqrel.MorphismsInterop]
B:32 [binder, in coqrel.KLR]
B:32 [binder, in coqrel.RelOperators]
B:345 [binder, in coqrel.RelOperators]
B:350 [binder, in coqrel.RelOperators]
B:352 [binder, in coqrel.RelOperators]
B:357 [binder, in coqrel.RelOperators]
B:36 [binder, in coqrel.RelDefinitions]
B:367 [binder, in coqrel.RelOperators]
B:376 [binder, in coqrel.RelOperators]
B:38 [binder, in coqrel.OptionRel]
B:38 [binder, in coqrel.RelClasses]
B:383 [binder, in coqrel.RelOperators]
B:39 [binder, in coqrel.Monotonicity]
B:392 [binder, in coqrel.RelOperators]
B:4 [binder, in coqrel.RDestruct]
B:4 [binder, in coqrel.MorphismsInterop]
B:40 [binder, in coqrel.MorphismsInterop]
B:401 [binder, in coqrel.RelOperators]
B:408 [binder, in coqrel.RelOperators]
B:418 [binder, in coqrel.RelOperators]
B:42 [binder, in coqrel.OptionRel]
B:42 [binder, in coqrel.RelClasses]
B:42 [binder, in coqrel.MorphismsInterop]
b:423 [binder, in coqrel.RelOperators]
B:427 [binder, in coqrel.RelOperators]
B:431 [binder, in coqrel.RelOperators]
B:44 [binder, in coqrel.OptionRel]
B:440 [binder, in coqrel.RelOperators]
B:45 [binder, in coqrel.LogicalRelationsTests]
B:48 [binder, in coqrel.Monotonicity]
B:48 [binder, in coqrel.MorphismsInterop]
B:49 [binder, in coqrel.RelOperators]
b:5 [binder, in coqrel.Transport]
b:5 [binder, in coqrel.PreOrderTactic]
B:5 [binder, in coqrel.RelDefinitions]
B:51 [binder, in coqrel.RelDefinitions]
B:52 [binder, in coqrel.OptionRel]
B:53 [binder, in coqrel.LogicalRelationsTests]
B:55 [binder, in coqrel.RelOperators]
B:56 [binder, in coqrel.Monotonicity]
B:56 [binder, in coqrel.MorphismsInterop]
b:57 [binder, in coqrel.OptionRel]
B:57 [binder, in coqrel.RelOperators]
B:59 [binder, in coqrel.OptionRel]
B:59 [binder, in coqrel.RelDefinitions]
B:60 [binder, in coqrel.LogicalRelationsTests]
B:62 [binder, in coqrel.Monotonicity]
B:63 [binder, in coqrel.RelOperators]
B:65 [binder, in coqrel.RelDefinitions]
B:67 [binder, in coqrel.LogicalRelationsTests]
B:68 [binder, in coqrel.RelOperators]
b:7 [binder, in coqrel.RelDefinitions]
b:7 [binder, in coqrel.LogicalRelationsTests]
B:73 [binder, in coqrel.RelOperators]
B:73 [binder, in coqrel.Monotonicity]
B:74 [binder, in coqrel.RelDefinitions]
b:74 [binder, in coqrel.LogicalRelationsTests]
b:76 [binder, in coqrel.LogicalRelationsTests]
B:79 [binder, in coqrel.RelDefinitions]
b:79 [binder, in coqrel.LogicalRelationsTests]
B:8 [binder, in coqrel.RelOperators]
B:8 [binder, in coqrel.Monotonicity]
b:82 [binder, in coqrel.LogicalRelationsTests]
B:83 [binder, in coqrel.Monotonicity]
b:87 [binder, in coqrel.LogicalRelationsTests]
B:88 [binder, in coqrel.RelDefinitions]
B:91 [binder, in coqrel.LogicalRelationsTests]
B:92 [binder, in coqrel.Monotonicity]
B:95 [binder, in coqrel.RelDefinitions]
B:97 [binder, in coqrel.Monotonicity]
B:98 [binder, in coqrel.RelOperators]
C
CandidateProperty [record, in coqrel.Monotonicity]CandidateProperty [inductive, in coqrel.Monotonicity]
candidate_related [projection, in coqrel.Monotonicity]
candidate_related [constructor, in coqrel.Monotonicity]
CommonPrefix [record, in coqrel.Monotonicity]
cons_rel [instance, in coqrel.Relators]
cons_rel_def [constructor, in coqrel.Relators]
convertible [projection, in coqrel.RelDefinitions]
Convertible [record, in coqrel.RelDefinitions]
convertible [constructor, in coqrel.RelDefinitions]
Convertible [inductive, in coqrel.RelDefinitions]
Coreflexive [record, in coqrel.RelClasses]
Coreflexive [inductive, in coqrel.RelClasses]
coreflexivity [projection, in coqrel.RelClasses]
coreflexivity [constructor, in coqrel.RelClasses]
curry [definition, in coqrel.RelOperators]
C1:133 [binder, in coqrel.KLR]
C1:153 [binder, in coqrel.LogicalRelationsTests]
C1:185 [binder, in coqrel.LogicalRelationsTests]
C1:307 [binder, in coqrel.RelOperators]
C1:314 [binder, in coqrel.RelOperators]
C1:326 [binder, in coqrel.RelOperators]
C2:136 [binder, in coqrel.KLR]
C2:154 [binder, in coqrel.LogicalRelationsTests]
C2:186 [binder, in coqrel.LogicalRelationsTests]
C2:310 [binder, in coqrel.RelOperators]
C2:317 [binder, in coqrel.RelOperators]
C2:329 [binder, in coqrel.RelOperators]
C:104 [binder, in coqrel.LogicalRelationsTests]
C:12 [binder, in coqrel.RelClasses]
C:127 [binder, in coqrel.LogicalRelationsTests]
C:132 [binder, in coqrel.Monotonicity]
c:133 [binder, in coqrel.LogicalRelationsTests]
C:144 [binder, in coqrel.Monotonicity]
C:150 [binder, in coqrel.RelOperators]
C:151 [binder, in coqrel.Monotonicity]
C:158 [binder, in coqrel.RelOperators]
C:161 [binder, in coqrel.RelOperators]
C:17 [binder, in coqrel.Monotonicity]
C:170 [binder, in coqrel.RelOperators]
C:177 [binder, in coqrel.RelOperators]
C:182 [binder, in coqrel.RelOperators]
C:214 [binder, in coqrel.LogicalRelationsTests]
C:28 [binder, in coqrel.RelClasses]
C:295 [binder, in coqrel.RelOperators]
C:30 [binder, in coqrel.Monotonicity]
C:301 [binder, in coqrel.RelOperators]
C:368 [binder, in coqrel.RelOperators]
c:372 [binder, in coqrel.RelOperators]
C:377 [binder, in coqrel.RelOperators]
c:381 [binder, in coqrel.RelOperators]
C:384 [binder, in coqrel.RelOperators]
c:390 [binder, in coqrel.RelOperators]
C:393 [binder, in coqrel.RelOperators]
c:397 [binder, in coqrel.RelOperators]
C:40 [binder, in coqrel.Monotonicity]
C:402 [binder, in coqrel.RelOperators]
c:404 [binder, in coqrel.RelOperators]
C:409 [binder, in coqrel.RelOperators]
c:415 [binder, in coqrel.RelOperators]
C:63 [binder, in coqrel.Monotonicity]
C:74 [binder, in coqrel.Monotonicity]
C:9 [binder, in coqrel.Monotonicity]
C:92 [binder, in coqrel.LogicalRelationsTests]
D
delay [definition, in coqrel.Delay]Delay [module, in coqrel.Delay]
Delay [library]
Delay.delayed_goal [definition, in coqrel.Delay]
Delay.open_conjunction_proj [projection, in coqrel.Delay]
Delay.open_conjunction [record, in coqrel.Delay]
Delay.unpack [definition, in coqrel.Delay]
direct_rexists [lemma, in coqrel.RelDefinitions]
D:133 [binder, in coqrel.Monotonicity]
D:171 [binder, in coqrel.RelOperators]
D:18 [binder, in coqrel.Monotonicity]
D:31 [binder, in coqrel.Monotonicity]
D:41 [binder, in coqrel.Monotonicity]
D:64 [binder, in coqrel.Monotonicity]
D:75 [binder, in coqrel.Monotonicity]
E
eapply [projection, in coqrel.Delay]EApply [record, in coqrel.Delay]
eapply [constructor, in coqrel.Delay]
EApply [inductive, in coqrel.Delay]
Empty_set_rel [inductive, in coqrel.Relators]
eqcl [definition, in coqrel.RelQuotient]
eqcl_reflection [lemma, in coqrel.RelQuotient]
eqcl_of_eq [instance, in coqrel.RelQuotient]
eqcl_of_le [instance, in coqrel.RelQuotient]
eqcl_surjective [lemma, in coqrel.RelQuotient]
eqcl_le_po [instance, in coqrel.RelQuotient]
eqcl_le_preo [instance, in coqrel.RelQuotient]
eqcl_params [instance, in coqrel.RelQuotient]
eqrel [definition, in coqrel.RelOperators]
eqrel_subrel [instance, in coqrel.RelOperators]
eqrel_equivalence [instance, in coqrel.RelOperators]
eq_corefl [instance, in coqrel.RelClasses]
eq_subrel [instance, in coqrel.RelDefinitions]
eq_candidate [instance, in coqrel.Monotonicity]
ex_monotonic_params [instance, in coqrel.Relators]
ex_monotonic [instance, in coqrel.Relators]
E:157 [binder, in coqrel.RelDefinitions]
e:169 [binder, in coqrel.RelDefinitions]
e:172 [binder, in coqrel.RelDefinitions]
e:175 [binder, in coqrel.RelDefinitions]
e:176 [binder, in coqrel.RelDefinitions]
e:177 [binder, in coqrel.RelDefinitions]
E:180 [binder, in coqrel.RelDefinitions]
e:190 [binder, in coqrel.RelDefinitions]
E:193 [binder, in coqrel.RelDefinitions]
e:201 [binder, in coqrel.RelDefinitions]
E:71 [binder, in coqrel.Relators]
E:87 [binder, in coqrel.Relators]
E:99 [binder, in coqrel.Relators]
F
false_leb [lemma, in coqrel.BoolRel]FE:164 [binder, in coqrel.RelDefinitions]
FE:185 [binder, in coqrel.RelDefinitions]
FE:46 [binder, in coqrel.Relators]
FE:56 [binder, in coqrel.Relators]
FE:78 [binder, in coqrel.Relators]
FE:92 [binder, in coqrel.Relators]
flip_rexists [lemma, in coqrel.RelDefinitions]
flip_rdestruct [lemma, in coqrel.RelDefinitions]
flip_relim [lemma, in coqrel.RelDefinitions]
flip_rintro [lemma, in coqrel.RelDefinitions]
flip_subrel_params [instance, in coqrel.RelDefinitions]
flip_subrel [instance, in coqrel.RelDefinitions]
flip_context_candidate [lemma, in coqrel.Monotonicity]
fold_impl_rstep [lemma, in coqrel.Relators]
fold_left_rel [instance, in coqrel.Relators]
fold_right_rel [instance, in coqrel.Relators]
forallp_relim [lemma, in coqrel.Relators]
forallp_rintro [lemma, in coqrel.Relators]
forallp_rel [definition, in coqrel.Relators]
forall_pointwise_relim [lemma, in coqrel.Relators]
forall_pointwise_rintro [lemma, in coqrel.Relators]
forall_pointwise_rel [definition, in coqrel.Relators]
forall_relim [lemma, in coqrel.RelDefinitions]
forall_rintro [lemma, in coqrel.RelDefinitions]
forall_rel [definition, in coqrel.RelDefinitions]
forall_relation_relim [lemma, in coqrel.MorphismsInterop]
forall_relation_rintro [lemma, in coqrel.MorphismsInterop]
forall_relation_params [instance, in coqrel.MorphismsInterop]
forall_relation_subrel [instance, in coqrel.MorphismsInterop]
fst_rel [instance, in coqrel.Relators]
FV1:100 [binder, in coqrel.Relators]
FV1:158 [binder, in coqrel.RelDefinitions]
FV1:194 [binder, in coqrel.RelDefinitions]
FV1:41 [binder, in coqrel.Relators]
FV1:53 [binder, in coqrel.Relators]
FV1:61 [binder, in coqrel.Relators]
FV1:72 [binder, in coqrel.Relators]
FV2:101 [binder, in coqrel.Relators]
FV2:159 [binder, in coqrel.RelDefinitions]
FV2:195 [binder, in coqrel.RelDefinitions]
FV2:42 [binder, in coqrel.Relators]
FV2:54 [binder, in coqrel.Relators]
FV2:62 [binder, in coqrel.Relators]
FV2:73 [binder, in coqrel.Relators]
f_equal_relim [lemma, in coqrel.Monotonicity]
F1:181 [binder, in coqrel.RelDefinitions]
F1:88 [binder, in coqrel.Relators]
F2:182 [binder, in coqrel.RelDefinitions]
F2:89 [binder, in coqrel.Relators]
f:103 [binder, in coqrel.Relators]
f:103 [binder, in coqrel.LogicalRelationsTests]
f:117 [binder, in coqrel.LogicalRelationsTests]
f:121 [binder, in coqrel.LogicalRelationsTests]
f:125 [binder, in coqrel.RelDefinitions]
f:129 [binder, in coqrel.LogicalRelationsTests]
f:139 [binder, in coqrel.RelDefinitions]
f:147 [binder, in coqrel.Monotonicity]
f:149 [binder, in coqrel.RelDefinitions]
f:15 [binder, in coqrel.Relators]
f:15 [binder, in coqrel.MorphismsInterop]
f:155 [binder, in coqrel.Monotonicity]
f:158 [binder, in coqrel.Monotonicity]
f:165 [binder, in coqrel.RelDefinitions]
f:18 [binder, in coqrel.LogicalRelationsTests]
f:186 [binder, in coqrel.RelDefinitions]
f:197 [binder, in coqrel.RelDefinitions]
f:203 [binder, in coqrel.RelOperators]
f:205 [binder, in coqrel.KLR]
f:207 [binder, in coqrel.LogicalRelationsTests]
f:212 [binder, in coqrel.RelOperators]
f:216 [binder, in coqrel.RelOperators]
f:218 [binder, in coqrel.LogicalRelationsTests]
f:22 [binder, in coqrel.Relators]
f:220 [binder, in coqrel.RelOperators]
f:228 [binder, in coqrel.RelOperators]
f:237 [binder, in coqrel.LogicalRelationsTests]
f:238 [binder, in coqrel.RelOperators]
f:243 [binder, in coqrel.LogicalRelationsTests]
f:247 [binder, in coqrel.RelOperators]
f:250 [binder, in coqrel.KLR]
f:258 [binder, in coqrel.RelOperators]
f:263 [binder, in coqrel.KLR]
f:269 [binder, in coqrel.RelOperators]
f:27 [binder, in coqrel.MorphismsInterop]
f:272 [binder, in coqrel.KLR]
f:273 [binder, in coqrel.RelOperators]
f:296 [binder, in coqrel.RelOperators]
f:302 [binder, in coqrel.RelOperators]
f:331 [binder, in coqrel.RelOperators]
f:34 [binder, in coqrel.MorphismsInterop]
f:35 [binder, in coqrel.Monotonicity]
f:35 [binder, in coqrel.LogicalRelationsTests]
f:44 [binder, in coqrel.Monotonicity]
f:44 [binder, in coqrel.MorphismsInterop]
f:47 [binder, in coqrel.Relators]
f:5 [binder, in coqrel.Relators]
f:50 [binder, in coqrel.Monotonicity]
f:50 [binder, in coqrel.MorphismsInterop]
f:57 [binder, in coqrel.Relators]
f:64 [binder, in coqrel.Relators]
f:65 [binder, in coqrel.LogicalRelationsTests]
f:69 [binder, in coqrel.Monotonicity]
f:7 [binder, in coqrel.MorphismsInterop]
f:79 [binder, in coqrel.Relators]
f:80 [binder, in coqrel.Monotonicity]
f:89 [binder, in coqrel.RelDefinitions]
f:93 [binder, in coqrel.Relators]
f:96 [binder, in coqrel.LogicalRelationsTests]
G
g:104 [binder, in coqrel.Relators]g:126 [binder, in coqrel.RelDefinitions]
g:140 [binder, in coqrel.RelDefinitions]
g:150 [binder, in coqrel.RelDefinitions]
g:159 [binder, in coqrel.Monotonicity]
g:16 [binder, in coqrel.Relators]
g:16 [binder, in coqrel.MorphismsInterop]
g:166 [binder, in coqrel.RelDefinitions]
g:187 [binder, in coqrel.RelDefinitions]
g:198 [binder, in coqrel.RelDefinitions]
g:204 [binder, in coqrel.RelOperators]
g:206 [binder, in coqrel.KLR]
g:208 [binder, in coqrel.LogicalRelationsTests]
g:213 [binder, in coqrel.RelOperators]
g:219 [binder, in coqrel.LogicalRelationsTests]
g:229 [binder, in coqrel.RelOperators]
g:23 [binder, in coqrel.Relators]
g:239 [binder, in coqrel.RelOperators]
g:245 [binder, in coqrel.LogicalRelationsTests]
g:248 [binder, in coqrel.RelOperators]
g:259 [binder, in coqrel.RelOperators]
g:270 [binder, in coqrel.RelOperators]
g:28 [binder, in coqrel.MorphismsInterop]
g:332 [binder, in coqrel.RelOperators]
g:35 [binder, in coqrel.MorphismsInterop]
g:36 [binder, in coqrel.Monotonicity]
g:45 [binder, in coqrel.Monotonicity]
g:45 [binder, in coqrel.MorphismsInterop]
g:48 [binder, in coqrel.Relators]
g:51 [binder, in coqrel.Monotonicity]
g:51 [binder, in coqrel.MorphismsInterop]
g:58 [binder, in coqrel.Relators]
g:6 [binder, in coqrel.Relators]
g:65 [binder, in coqrel.Relators]
g:70 [binder, in coqrel.Monotonicity]
g:8 [binder, in coqrel.MorphismsInterop]
g:80 [binder, in coqrel.Relators]
g:81 [binder, in coqrel.Monotonicity]
g:90 [binder, in coqrel.RelDefinitions]
g:94 [binder, in coqrel.Relators]
H
HopA:175 [binder, in coqrel.LogicalRelationsTests]HopB:176 [binder, in coqrel.LogicalRelationsTests]
Hop:48 [binder, in coqrel.LogicalRelationsTests]
HR:12 [binder, in coqrel.LogicalRelationsTests]
HR:247 [binder, in coqrel.Relators]
HR:25 [binder, in coqrel.RelQuotient]
HR:26 [binder, in coqrel.RelQuotient]
HR:268 [binder, in coqrel.Relators]
HR:27 [binder, in coqrel.RelQuotient]
HR:271 [binder, in coqrel.Relators]
HR:274 [binder, in coqrel.Relators]
HR:277 [binder, in coqrel.Relators]
HT:10 [binder, in coqrel.Delay]
Hux:14 [binder, in coqrel.PreOrderTactic]
Hw':158 [binder, in coqrel.KLR]
Hxa:177 [binder, in coqrel.LogicalRelationsTests]
Hxb:178 [binder, in coqrel.LogicalRelationsTests]
Hxy:51 [binder, in coqrel.LogicalRelationsTests]
Hya:179 [binder, in coqrel.LogicalRelationsTests]
Hyb:180 [binder, in coqrel.LogicalRelationsTests]
h1:19 [binder, in coqrel.Monotonicity]
H1:19 [binder, in coqrel.BoolRel]
H1:7 [binder, in coqrel.BoolRel]
H1:9 [binder, in coqrel.BoolRel]
H2:10 [binder, in coqrel.BoolRel]
H2:18 [binder, in coqrel.BoolRel]
h2:20 [binder, in coqrel.Monotonicity]
H2:8 [binder, in coqrel.BoolRel]
h:10 [binder, in coqrel.Monotonicity]
H:126 [binder, in coqrel.Relators]
H:13 [binder, in coqrel.LogicalRelationsTests]
H:144 [binder, in coqrel.Relators]
H:16 [binder, in coqrel.PreOrderTactic]
H:191 [binder, in coqrel.RelOperators]
H:198 [binder, in coqrel.RelOperators]
H:199 [binder, in coqrel.LogicalRelationsTests]
h:230 [binder, in coqrel.RelOperators]
H:25 [binder, in coqrel.RelClasses]
H:31 [binder, in coqrel.Relators]
H:32 [binder, in coqrel.LogicalRelationsTests]
H:39 [binder, in coqrel.Relators]
H:49 [binder, in coqrel.RelDefinitions]
H:64 [binder, in coqrel.Transport]
I
implb_leb [instance, in coqrel.BoolRel]impl_transport [lemma, in coqrel.Transport]
inl_rel [instance, in coqrel.Relators]
inl_rel_def [constructor, in coqrel.Relators]
inr_rel [instance, in coqrel.Relators]
inr_rel_def [constructor, in coqrel.Relators]
in_eqcl_wf [projection, in coqrel.RelQuotient]
in_eqcl [projection, in coqrel.RelQuotient]
I:359 [binder, in coqrel.RelOperators]
I:365 [binder, in coqrel.RelOperators]
K
k [definition, in coqrel.KLR]kf:139 [binder, in coqrel.KLR]
kf:200 [binder, in coqrel.KLR]
kf:223 [binder, in coqrel.KLR]
kf:26 [binder, in coqrel.KLR]
kf:90 [binder, in coqrel.KLR]
klr [definition, in coqrel.KLR]
KLR [library]
klr_pullw_relim [lemma, in coqrel.KLR]
klr_pullw_rintro [lemma, in coqrel.KLR]
klr_pullw_subrel_params [instance, in coqrel.KLR]
klr_pullw_subrel [instance, in coqrel.KLR]
klr_pullw [definition, in coqrel.KLR]
klr_diamat [definition, in coqrel.KLR]
klr_boxto [definition, in coqrel.KLR]
klr_diam_subrel_params [instance, in coqrel.KLR]
klr_box_subrel_params [instance, in coqrel.KLR]
klr_diam_relim [lemma, in coqrel.KLR]
klr_diam_rintro [lemma, in coqrel.KLR]
klr_diam_subrel [instance, in coqrel.KLR]
klr_diam [definition, in coqrel.KLR]
klr_box_relim [lemma, in coqrel.KLR]
klr_box_rintro [lemma, in coqrel.KLR]
klr_box_subrel [instance, in coqrel.KLR]
klr_box [definition, in coqrel.KLR]
klr_curry [definition, in coqrel.KLR]
klr_inter [definition, in coqrel.KLR]
klr_union [definition, in coqrel.KLR]
klr_inr [constructor, in coqrel.KLR]
klr_inl [constructor, in coqrel.KLR]
klr_sum [inductive, in coqrel.KLR]
KripkeFrame [record, in coqrel.KLR]
k_rel_params [instance, in coqrel.KLR]
k_relim [lemma, in coqrel.KLR]
k_rintro [lemma, in coqrel.KLR]
k_rel [instance, in coqrel.KLR]
k1 [definition, in coqrel.KLR]
k1_rel_params [instance, in coqrel.KLR]
k1_relim [lemma, in coqrel.KLR]
k1_rintro [lemma, in coqrel.KLR]
k1_rel [instance, in coqrel.KLR]
k2 [definition, in coqrel.KLR]
k2_rel_params [instance, in coqrel.KLR]
k2_unfold [instance, in coqrel.KLR]
k2_relim [lemma, in coqrel.KLR]
k2_rintro [lemma, in coqrel.KLR]
k2_rel [instance, in coqrel.KLR]
L
leb_transport_eq_true [instance, in coqrel.BoolRel]leb_rdestruct [lemma, in coqrel.BoolRel]
leb_preo [instance, in coqrel.BoolRel]
left_le [constructor, in coqrel.BoolRel]
left_rel [instance, in coqrel.BoolRel]
left_rel_def [constructor, in coqrel.BoolRel]
length_rel [instance, in coqrel.Relators]
LIFT [section, in coqrel.KLR]
list_rel_trans [lemma, in coqrel.Relators]
list_rel_sym [lemma, in coqrel.Relators]
list_rel_corefl [lemma, in coqrel.Relators]
list_rel_refl [lemma, in coqrel.Relators]
list_subrel_params [instance, in coqrel.Relators]
list_subrel [instance, in coqrel.Relators]
list_rel [inductive, in coqrel.Relators]
list_klr [definition, in coqrel.KLR]
LogicalRelations [library]
LogicalRelationsTests [library]
lsat [definition, in coqrel.RelOperators]
lsat_subrel_params [instance, in coqrel.RelOperators]
lsat_subrel [instance, in coqrel.RelOperators]
L1:198 [binder, in coqrel.KLR]
l1:207 [binder, in coqrel.KLR]
l1:215 [binder, in coqrel.KLR]
l1:231 [binder, in coqrel.LogicalRelationsTests]
L2:199 [binder, in coqrel.KLR]
l2:208 [binder, in coqrel.KLR]
l2:218 [binder, in coqrel.KLR]
l2:232 [binder, in coqrel.LogicalRelationsTests]
l:142 [binder, in coqrel.KLR]
l:152 [binder, in coqrel.KLR]
l:161 [binder, in coqrel.KLR]
l:171 [binder, in coqrel.KLR]
l:181 [binder, in coqrel.KLR]
l:189 [binder, in coqrel.KLR]
L:4 [binder, in coqrel.KLR]
M
map_rel [instance, in coqrel.Relators]MODALITIES [section, in coqrel.KLR]
Monotonic [abbreviation, in coqrel.RelDefinitions]
monotonicity [projection, in coqrel.Monotonicity]
Monotonicity [record, in coqrel.Monotonicity]
monotonicity [constructor, in coqrel.Monotonicity]
Monotonicity [inductive, in coqrel.Monotonicity]
Monotonicity [library]
monotonicity_rstep [instance, in coqrel.Monotonicity]
MorphismsInterop [library]
morphisms_proper_related [instance, in coqrel.MorphismsInterop]
m1:12 [binder, in coqrel.Monotonicity]
m1:145 [binder, in coqrel.Monotonicity]
m1:153 [binder, in coqrel.Monotonicity]
m1:23 [binder, in coqrel.Monotonicity]
m1:3 [binder, in coqrel.Monotonicity]
m1:33 [binder, in coqrel.Monotonicity]
m1:42 [binder, in coqrel.Monotonicity]
m1:59 [binder, in coqrel.Monotonicity]
m1:66 [binder, in coqrel.Monotonicity]
m1:77 [binder, in coqrel.Monotonicity]
m2:13 [binder, in coqrel.Monotonicity]
m2:146 [binder, in coqrel.Monotonicity]
m2:154 [binder, in coqrel.Monotonicity]
m2:24 [binder, in coqrel.Monotonicity]
m2:34 [binder, in coqrel.Monotonicity]
m2:4 [binder, in coqrel.Monotonicity]
m2:43 [binder, in coqrel.Monotonicity]
m2:60 [binder, in coqrel.Monotonicity]
m2:67 [binder, in coqrel.Monotonicity]
m2:78 [binder, in coqrel.Monotonicity]
m:100 [binder, in coqrel.Monotonicity]
m:115 [binder, in coqrel.Monotonicity]
m:12 [binder, in coqrel.RDestruct]
m:124 [binder, in coqrel.Monotonicity]
m:135 [binder, in coqrel.Monotonicity]
m:151 [binder, in coqrel.RelDefinitions]
m:160 [binder, in coqrel.Monotonicity]
m:17 [binder, in coqrel.MorphismsInterop]
m:209 [binder, in coqrel.RelDefinitions]
m:21 [binder, in coqrel.RDestruct]
m:214 [binder, in coqrel.RelDefinitions]
m:230 [binder, in coqrel.RelDefinitions]
m:236 [binder, in coqrel.RelDefinitions]
m:24 [binder, in coqrel.Relators]
m:28 [binder, in coqrel.RDestruct]
m:379 [binder, in coqrel.RelOperators]
m:39 [binder, in coqrel.RelDefinitions]
m:405 [binder, in coqrel.RelOperators]
m:436 [binder, in coqrel.RelOperators]
m:5 [binder, in coqrel.RDestruct]
m:54 [binder, in coqrel.RelDefinitions]
m:56 [binder, in coqrel.LogicalRelationsTests]
m:62 [binder, in coqrel.RelDefinitions]
m:67 [binder, in coqrel.RelDefinitions]
m:76 [binder, in coqrel.RelDefinitions]
m:8 [binder, in coqrel.PreOrderTactic]
m:83 [binder, in coqrel.RelDefinitions]
m:94 [binder, in coqrel.Monotonicity]
m:97 [binder, in coqrel.RelDefinitions]
N
negb_leb [instance, in coqrel.BoolRel]nil_rel [instance, in coqrel.Relators]
nil_rel_def [constructor, in coqrel.Relators]
nondelayed [projection, in coqrel.Delay]
NonDelayed [record, in coqrel.Delay]
nondelayed [constructor, in coqrel.Delay]
NonDelayed [inductive, in coqrel.Delay]
None_ge [lemma, in coqrel.OptionRel]
None_ge_def [constructor, in coqrel.OptionRel]
None_le [lemma, in coqrel.OptionRel]
None_le_def [constructor, in coqrel.OptionRel]
None_rel [instance, in coqrel.Relators]
None_rel_def [constructor, in coqrel.Relators]
NotEvar [record, in coqrel.RelDefinitions]
n:101 [binder, in coqrel.Monotonicity]
n:116 [binder, in coqrel.Monotonicity]
n:125 [binder, in coqrel.Monotonicity]
n:13 [binder, in coqrel.RDestruct]
n:136 [binder, in coqrel.Monotonicity]
n:14 [binder, in coqrel.Monotonicity]
n:152 [binder, in coqrel.RelDefinitions]
n:161 [binder, in coqrel.Monotonicity]
n:18 [binder, in coqrel.MorphismsInterop]
n:210 [binder, in coqrel.RelDefinitions]
n:215 [binder, in coqrel.RelDefinitions]
n:22 [binder, in coqrel.RDestruct]
n:231 [binder, in coqrel.RelDefinitions]
n:237 [binder, in coqrel.RelDefinitions]
n:25 [binder, in coqrel.Relators]
n:25 [binder, in coqrel.Monotonicity]
n:29 [binder, in coqrel.RDestruct]
n:32 [binder, in coqrel.Monotonicity]
n:380 [binder, in coqrel.RelOperators]
n:40 [binder, in coqrel.RelDefinitions]
n:406 [binder, in coqrel.RelOperators]
n:437 [binder, in coqrel.RelOperators]
n:5 [binder, in coqrel.Monotonicity]
n:55 [binder, in coqrel.RelDefinitions]
n:57 [binder, in coqrel.LogicalRelationsTests]
n:6 [binder, in coqrel.RDestruct]
n:63 [binder, in coqrel.RelDefinitions]
n:68 [binder, in coqrel.RelDefinitions]
n:71 [binder, in coqrel.Monotonicity]
n:77 [binder, in coqrel.RelDefinitions]
n:84 [binder, in coqrel.RelDefinitions]
n:95 [binder, in coqrel.Monotonicity]
n:98 [binder, in coqrel.RelDefinitions]
O
once [projection, in coqrel.RelDefinitions]Once [record, in coqrel.RelDefinitions]
once [constructor, in coqrel.RelDefinitions]
Once [inductive, in coqrel.RelDefinitions]
opA:171 [binder, in coqrel.LogicalRelationsTests]
opB:172 [binder, in coqrel.LogicalRelationsTests]
OptionRel [library]
option_ge_transport_eq_none [instance, in coqrel.OptionRel]
option_le_transport_eq_some [instance, in coqrel.OptionRel]
option_map_ge [instance, in coqrel.OptionRel]
option_ge_trans [lemma, in coqrel.OptionRel]
option_ge_refl [lemma, in coqrel.OptionRel]
option_ge_rel [instance, in coqrel.OptionRel]
option_ge_subrel_params [instance, in coqrel.OptionRel]
option_ge_subrel [instance, in coqrel.OptionRel]
option_ge [inductive, in coqrel.OptionRel]
option_map_le [instance, in coqrel.OptionRel]
option_le_trans [lemma, in coqrel.OptionRel]
option_le_refl [lemma, in coqrel.OptionRel]
option_le_rel [instance, in coqrel.OptionRel]
option_le_subrel_params [instance, in coqrel.OptionRel]
option_le_subrel [instance, in coqrel.OptionRel]
option_le [inductive, in coqrel.OptionRel]
option_rel_some_inv [lemma, in coqrel.Relators]
option_map_rel [instance, in coqrel.Relators]
option_rel_refl [lemma, in coqrel.Relators]
option_subrel_params [instance, in coqrel.Relators]
option_subrel [instance, in coqrel.Relators]
option_rel [inductive, in coqrel.Relators]
op:47 [binder, in coqrel.LogicalRelationsTests]
orb_leb [instance, in coqrel.BoolRel]
or_monotonic [instance, in coqrel.Relators]
P
pair_rel [instance, in coqrel.Relators]pat:216 [binder, in coqrel.KLR]
pat:219 [binder, in coqrel.KLR]
PA:6 [binder, in coqrel.Transport]
PB:7 [binder, in coqrel.Transport]
pointwise_relation_subrel_subrel [instance, in coqrel.MorphismsInterop]
pointwise_relation_relim [lemma, in coqrel.MorphismsInterop]
pointwise_relation_rintro [lemma, in coqrel.MorphismsInterop]
pointwise_relation_params [instance, in coqrel.MorphismsInterop]
pointwise_relation_subrel [instance, in coqrel.MorphismsInterop]
PolarityResolved [record, in coqrel.RelDefinitions]
PreOrderTactic [library]
prod_rel_transport_eq_pair [instance, in coqrel.Transport]
prod_rel_preorder [lemma, in coqrel.Relators]
prod_rel_sym [lemma, in coqrel.Relators]
prod_rel_trans [lemma, in coqrel.Relators]
prod_rel_corefl [lemma, in coqrel.Relators]
prod_rel_refl [lemma, in coqrel.Relators]
prod_rdestruct [instance, in coqrel.Relators]
prod_subrel_params [instance, in coqrel.Relators]
prod_subrel [instance, in coqrel.Relators]
prod_rel [definition, in coqrel.Relators]
prod_klr [definition, in coqrel.KLR]
PROPERTIES [section, in coqrel.RelQuotient]
psat [inductive, in coqrel.RelOperators]
psat_corefl [lemma, in coqrel.RelOperators]
psat_subrel_params [instance, in coqrel.RelOperators]
psat_subrel [instance, in coqrel.RelOperators]
psat_intro [constructor, in coqrel.RelOperators]
P1:1 [binder, in coqrel.BoolRel]
P1:11 [binder, in coqrel.BoolRel]
p1:21 [binder, in coqrel.Monotonicity]
P2:12 [binder, in coqrel.BoolRel]
P2:2 [binder, in coqrel.BoolRel]
p2:22 [binder, in coqrel.Monotonicity]
P:1 [binder, in coqrel.Delay]
P:1 [binder, in coqrel.LogicalRelationsTests]
P:107 [binder, in coqrel.Relators]
P:108 [binder, in coqrel.Monotonicity]
P:11 [binder, in coqrel.Delay]
p:11 [binder, in coqrel.Monotonicity]
P:117 [binder, in coqrel.RelDefinitions]
P:117 [binder, in coqrel.Monotonicity]
P:122 [binder, in coqrel.Monotonicity]
P:126 [binder, in coqrel.Monotonicity]
P:132 [binder, in coqrel.RelOperators]
P:137 [binder, in coqrel.Monotonicity]
P:15 [binder, in coqrel.RDestruct]
P:15 [binder, in coqrel.RelDefinitions]
P:153 [binder, in coqrel.RelDefinitions]
P:162 [binder, in coqrel.Monotonicity]
P:167 [binder, in coqrel.KLR]
p:19 [binder, in coqrel.LogicalRelationsTests]
P:19 [binder, in coqrel.MorphismsInterop]
P:194 [binder, in coqrel.KLR]
P:20 [binder, in coqrel.RelDefinitions]
P:202 [binder, in coqrel.RelDefinitions]
P:209 [binder, in coqrel.Relators]
P:21 [binder, in coqrel.BoolRel]
P:216 [binder, in coqrel.RelDefinitions]
P:22 [binder, in coqrel.MorphismsInterop]
P:222 [binder, in coqrel.RelDefinitions]
P:244 [binder, in coqrel.KLR]
P:252 [binder, in coqrel.RelOperators]
P:26 [binder, in coqrel.Relators]
P:27 [binder, in coqrel.RelDefinitions]
P:277 [binder, in coqrel.KLR]
P:30 [binder, in coqrel.RelDefinitions]
P:333 [binder, in coqrel.RelOperators]
P:346 [binder, in coqrel.RelOperators]
P:353 [binder, in coqrel.RelOperators]
P:37 [binder, in coqrel.RelDefinitions]
P:37 [binder, in coqrel.MorphismsInterop]
P:388 [binder, in coqrel.RelOperators]
P:4 [binder, in coqrel.Delay]
P:413 [binder, in coqrel.RelOperators]
P:44 [binder, in coqrel.KLR]
P:447 [binder, in coqrel.RelOperators]
P:5 [binder, in coqrel.Delay]
P:52 [binder, in coqrel.RelDefinitions]
P:53 [binder, in coqrel.MorphismsInterop]
P:55 [binder, in coqrel.Transport]
P:6 [binder, in coqrel.Delay]
P:60 [binder, in coqrel.RelDefinitions]
P:61 [binder, in coqrel.KLR]
P:67 [binder, in coqrel.Relators]
P:69 [binder, in coqrel.RelDefinitions]
P:7 [binder, in coqrel.Delay]
P:82 [binder, in coqrel.KLR]
P:85 [binder, in coqrel.RelDefinitions]
P:87 [binder, in coqrel.Monotonicity]
Q
qle [definition, in coqrel.RelQuotient]QueryParams [record, in coqrel.Monotonicity]
query_params_both [lemma, in coqrel.Monotonicity]
query_params_one [lemma, in coqrel.Monotonicity]
quotient [record, in coqrel.RelQuotient]
Q':119 [binder, in coqrel.Monotonicity]
Q':335 [binder, in coqrel.RelOperators]
Q1:13 [binder, in coqrel.BoolRel]
Q1:3 [binder, in coqrel.BoolRel]
Q2:14 [binder, in coqrel.BoolRel]
Q2:4 [binder, in coqrel.BoolRel]
Q:108 [binder, in coqrel.Relators]
Q:109 [binder, in coqrel.Monotonicity]
Q:118 [binder, in coqrel.RelDefinitions]
Q:118 [binder, in coqrel.Monotonicity]
Q:12 [binder, in coqrel.Delay]
Q:127 [binder, in coqrel.Monotonicity]
Q:154 [binder, in coqrel.RelDefinitions]
Q:16 [binder, in coqrel.RDestruct]
Q:163 [binder, in coqrel.Monotonicity]
Q:168 [binder, in coqrel.KLR]
Q:195 [binder, in coqrel.KLR]
Q:2 [binder, in coqrel.LogicalRelationsTests]
Q:20 [binder, in coqrel.MorphismsInterop]
Q:203 [binder, in coqrel.RelDefinitions]
Q:21 [binder, in coqrel.RelDefinitions]
Q:217 [binder, in coqrel.RelDefinitions]
Q:23 [binder, in coqrel.RDestruct]
Q:24 [binder, in coqrel.RelDefinitions]
Q:245 [binder, in coqrel.KLR]
Q:253 [binder, in coqrel.RelOperators]
Q:27 [binder, in coqrel.Relators]
Q:278 [binder, in coqrel.KLR]
Q:30 [binder, in coqrel.RDestruct]
Q:31 [binder, in coqrel.RelDefinitions]
Q:334 [binder, in coqrel.RelOperators]
Q:38 [binder, in coqrel.MorphismsInterop]
Q:389 [binder, in coqrel.RelOperators]
Q:414 [binder, in coqrel.RelOperators]
Q:45 [binder, in coqrel.KLR]
Q:52 [binder, in coqrel.Monotonicity]
Q:54 [binder, in coqrel.MorphismsInterop]
Q:56 [binder, in coqrel.Transport]
Q:62 [binder, in coqrel.KLR]
Q:67 [binder, in coqrel.Transport]
Q:68 [binder, in coqrel.Relators]
Q:7 [binder, in coqrel.RDestruct]
Q:70 [binder, in coqrel.RelDefinitions]
Q:83 [binder, in coqrel.KLR]
Q:88 [binder, in coqrel.Monotonicity]
R
RAB:13 [binder, in coqrel.RelClasses]RAB:151 [binder, in coqrel.RelOperators]
RAB:172 [binder, in coqrel.RelOperators]
RAB:178 [binder, in coqrel.RelOperators]
RAB:183 [binder, in coqrel.RelOperators]
RAB:29 [binder, in coqrel.RelClasses]
RAC:15 [binder, in coqrel.RelClasses]
RAC:31 [binder, in coqrel.RelClasses]
rauto [projection, in coqrel.RelDefinitions]
RAuto [record, in coqrel.RelDefinitions]
rauto [constructor, in coqrel.RelDefinitions]
RAuto [inductive, in coqrel.RelDefinitions]
RAutoSubgoals [record, in coqrel.RelDefinitions]
RAutoSubgoals [inductive, in coqrel.RelDefinitions]
rauto_rstep [instance, in coqrel.RelDefinitions]
rauto_subgoals [projection, in coqrel.RelDefinitions]
rauto_subgoals [constructor, in coqrel.RelDefinitions]
RAuto0:65 [binder, in coqrel.Transport]
RA12:48 [binder, in coqrel.RelClasses]
RA13:50 [binder, in coqrel.RelClasses]
RA23:49 [binder, in coqrel.RelClasses]
RA:123 [binder, in coqrel.RelDefinitions]
RA:13 [binder, in coqrel.MorphismsInterop]
RA:137 [binder, in coqrel.RelDefinitions]
RA:14 [binder, in coqrel.KLR]
RA:147 [binder, in coqrel.RelDefinitions]
RA:153 [binder, in coqrel.Relators]
RA:157 [binder, in coqrel.Relators]
RA:159 [binder, in coqrel.Relators]
RA:173 [binder, in coqrel.LogicalRelationsTests]
RA:189 [binder, in coqrel.Relators]
RA:193 [binder, in coqrel.Relators]
RA:195 [binder, in coqrel.Relators]
RA:197 [binder, in coqrel.Relators]
RA:207 [binder, in coqrel.Relators]
RA:22 [binder, in coqrel.LogicalRelationsTests]
RA:236 [binder, in coqrel.Relators]
RA:24 [binder, in coqrel.OptionRel]
RA:248 [binder, in coqrel.Relators]
RA:28 [binder, in coqrel.OptionRel]
RA:280 [binder, in coqrel.Relators]
RA:282 [binder, in coqrel.Relators]
RA:284 [binder, in coqrel.Relators]
RA:3 [binder, in coqrel.OptionRel]
RA:39 [binder, in coqrel.RelClasses]
RA:43 [binder, in coqrel.RelClasses]
RA:49 [binder, in coqrel.OptionRel]
RA:5 [binder, in coqrel.MorphismsInterop]
RA:54 [binder, in coqrel.LogicalRelationsTests]
RA:61 [binder, in coqrel.LogicalRelationsTests]
RA:68 [binder, in coqrel.LogicalRelationsTests]
RBC:14 [binder, in coqrel.RelClasses]
RBC:152 [binder, in coqrel.RelOperators]
RBC:173 [binder, in coqrel.RelOperators]
RBC:179 [binder, in coqrel.RelOperators]
RBC:184 [binder, in coqrel.RelOperators]
RBC:30 [binder, in coqrel.RelClasses]
RB12:54 [binder, in coqrel.RelClasses]
RB13:56 [binder, in coqrel.RelClasses]
RB23:55 [binder, in coqrel.RelClasses]
RB:124 [binder, in coqrel.RelDefinitions]
RB:138 [binder, in coqrel.RelDefinitions]
RB:14 [binder, in coqrel.MorphismsInterop]
RB:148 [binder, in coqrel.RelDefinitions]
RB:15 [binder, in coqrel.KLR]
RB:154 [binder, in coqrel.Relators]
RB:158 [binder, in coqrel.Relators]
RB:160 [binder, in coqrel.Relators]
RB:174 [binder, in coqrel.LogicalRelationsTests]
RB:190 [binder, in coqrel.Relators]
RB:194 [binder, in coqrel.Relators]
RB:196 [binder, in coqrel.Relators]
RB:198 [binder, in coqrel.Relators]
RB:208 [binder, in coqrel.Relators]
RB:249 [binder, in coqrel.Relators]
RB:25 [binder, in coqrel.OptionRel]
RB:25 [binder, in coqrel.LogicalRelationsTests]
RB:281 [binder, in coqrel.Relators]
RB:283 [binder, in coqrel.Relators]
RB:285 [binder, in coqrel.Relators]
RB:4 [binder, in coqrel.Relators]
RB:40 [binder, in coqrel.RelClasses]
RB:44 [binder, in coqrel.RelClasses]
RB:50 [binder, in coqrel.OptionRel]
RB:55 [binder, in coqrel.LogicalRelationsTests]
RB:6 [binder, in coqrel.MorphismsInterop]
RB:62 [binder, in coqrel.LogicalRelationsTests]
RB:69 [binder, in coqrel.LogicalRelationsTests]
RCD:174 [binder, in coqrel.RelOperators]
rcompose [projection, in coqrel.RelClasses]
RCompose [record, in coqrel.RelClasses]
rcompose [constructor, in coqrel.RelClasses]
RCompose [inductive, in coqrel.RelClasses]
rcompose_transitive [instance, in coqrel.RelClasses]
rcompose_subrel [instance, in coqrel.RelOperators]
Rc:138 [binder, in coqrel.Monotonicity]
Rc:235 [binder, in coqrel.RelDefinitions]
rdecompose [projection, in coqrel.RelClasses]
RDecompose [record, in coqrel.RelClasses]
rdecompose [constructor, in coqrel.RelClasses]
RDecompose [inductive, in coqrel.RelClasses]
rdecompose_subrel [instance, in coqrel.RelOperators]
rdestruct [projection, in coqrel.RelDefinitions]
RDestruct [record, in coqrel.RelDefinitions]
rdestruct [constructor, in coqrel.RelDefinitions]
RDestruct [inductive, in coqrel.RelDefinitions]
RDestruct [library]
rdestruct_remember_rintro [lemma, in coqrel.RDestruct]
rdestruct_forget_rintro [lemma, in coqrel.RDestruct]
rdestruct_remember_intro [constructor, in coqrel.RDestruct]
rdestruct_remember [inductive, in coqrel.RDestruct]
rdestruct_rstep [lemma, in coqrel.RDestruct]
rdestruct_result [definition, in coqrel.RDestruct]
reflexivity_rstep [lemma, in coqrel.RelDefinitions]
rel [definition, in coqrel.RelDefinitions]
related [projection, in coqrel.RelDefinitions]
Related [record, in coqrel.RelDefinitions]
related [constructor, in coqrel.RelDefinitions]
Related [inductive, in coqrel.RelDefinitions]
Relators [library]
RelClasses [library]
RelDefinitions [library]
relim [projection, in coqrel.RelDefinitions]
RElim [record, in coqrel.RelDefinitions]
relim [constructor, in coqrel.RelDefinitions]
RElim [inductive, in coqrel.RelDefinitions]
relim_base [instance, in coqrel.RelDefinitions]
RelOperators [library]
RelQuotient [library]
rel_curry2_set_le_transport [lemma, in coqrel.Transport]
rel_curry_set_le_transport [lemma, in coqrel.Transport]
rel_kvd_subrel_params [instance, in coqrel.KLR]
rel_kvd_relim [lemma, in coqrel.KLR]
rel_kvd_rintro [lemma, in coqrel.KLR]
rel_kvd_subrel [instance, in coqrel.KLR]
rel_kvd [definition, in coqrel.KLR]
rel_incr_rdestruct [lemma, in coqrel.RelOperators]
rel_incr_rintro [lemma, in coqrel.RelOperators]
rel_incr_subrel_params [instance, in coqrel.RelOperators]
rel_incr_subrel [instance, in coqrel.RelOperators]
rel_incr [definition, in coqrel.RelOperators]
rel_ex_relim [lemma, in coqrel.RelOperators]
rel_ex_rintro [lemma, in coqrel.RelOperators]
rel_ex [definition, in coqrel.RelOperators]
rel_all_relim [lemma, in coqrel.RelOperators]
rel_all_rintro [lemma, in coqrel.RelOperators]
rel_all [definition, in coqrel.RelOperators]
rel_curry_relim [lemma, in coqrel.RelOperators]
rel_uncurry [definition, in coqrel.RelOperators]
rel_curry [definition, in coqrel.RelOperators]
rel_push_snd_rexists [lemma, in coqrel.RelOperators]
rel_push_fst_rexists [lemma, in coqrel.RelOperators]
rel_push_corefl [lemma, in coqrel.RelOperators]
rel_push_subrel_params [instance, in coqrel.RelOperators]
rel_push_subrel [instance, in coqrel.RelOperators]
rel_push_rintro [constructor, in coqrel.RelOperators]
rel_push [inductive, in coqrel.RelOperators]
rel_pull_relim [lemma, in coqrel.RelOperators]
rel_pull_rintro [lemma, in coqrel.RelOperators]
rel_pull_rcompose [lemma, in coqrel.RelOperators]
rel_pull_sym [lemma, in coqrel.RelOperators]
rel_pull_refl [lemma, in coqrel.RelOperators]
rel_pull_subrel_params [instance, in coqrel.RelOperators]
rel_pull_subrel [instance, in coqrel.RelOperators]
rel_pull [definition, in coqrel.RelOperators]
rel_compose_rdecompose [instance, in coqrel.RelOperators]
rel_compose_rcompose [instance, in coqrel.RelOperators]
rel_compose_assoc [lemma, in coqrel.RelOperators]
rel_compose_id_right [lemma, in coqrel.RelOperators]
rel_compose_id_left [lemma, in coqrel.RelOperators]
rel_compose_params [instance, in coqrel.RelOperators]
rel_compose_eqrel [instance, in coqrel.RelOperators]
rel_compose_subrel [instance, in coqrel.RelOperators]
rel_compose [definition, in coqrel.RelOperators]
rel_top_equiv [instance, in coqrel.RelOperators]
rel_top_rintro [lemma, in coqrel.RelOperators]
rel_top [definition, in coqrel.RelOperators]
rel_bot_relim [lemma, in coqrel.RelOperators]
rel_bot_subrel [lemma, in coqrel.RelOperators]
rel_bot [definition, in coqrel.RelOperators]
rel_impl_subrel_codomain [lemma, in coqrel.RelOperators]
rel_impl_relim [lemma, in coqrel.RelOperators]
rel_impl_rintro [lemma, in coqrel.RelOperators]
rel_impl_subrel_params [instance, in coqrel.RelOperators]
rel_impl_subrel [instance, in coqrel.RelOperators]
rel_impl [definition, in coqrel.RelOperators]
rel_inter_flip_sym [instance, in coqrel.RelOperators]
rel_inter_sym [lemma, in coqrel.RelOperators]
rel_inter_trans [lemma, in coqrel.RelOperators]
rel_inter_corefl_r [lemma, in coqrel.RelOperators]
rel_inter_corefl_l [lemma, in coqrel.RelOperators]
rel_inter_refl [lemma, in coqrel.RelOperators]
rel_inter_glb [lemma, in coqrel.RelOperators]
rel_inter_subrel_rexists_r [lemma, in coqrel.RelOperators]
rel_inter_subrel_rexists_l [lemma, in coqrel.RelOperators]
rel_inter_rexists [lemma, in coqrel.RelOperators]
rel_inter_params [instance, in coqrel.RelOperators]
rel_inter_subrel [instance, in coqrel.RelOperators]
rel_inter [definition, in coqrel.RelOperators]
rel_union_sym [lemma, in coqrel.RelOperators]
rel_union_corefl [lemma, in coqrel.RelOperators]
rel_union_refl_r [lemma, in coqrel.RelOperators]
rel_union_refl_l [lemma, in coqrel.RelOperators]
rel_union_lub [lemma, in coqrel.RelOperators]
rel_union_subrel_rexists_r [lemma, in coqrel.RelOperators]
rel_union_subrel_rexists_l [lemma, in coqrel.RelOperators]
rel_union_rexists_r [lemma, in coqrel.RelOperators]
rel_union_rexists_l [lemma, in coqrel.RelOperators]
rel_union_subrel_params [instance, in coqrel.RelOperators]
rel_union_subrel [instance, in coqrel.RelOperators]
rel_union [definition, in coqrel.RelOperators]
rel_top_component_trsym [lemma, in coqrel.LogicalRelationsTests]
rel_top_component_refl [lemma, in coqrel.LogicalRelationsTests]
rel_ex_1 [lemma, in coqrel.LogicalRelationsTests]
rel_all_1 [lemma, in coqrel.LogicalRelationsTests]
rel_pull_2 [lemma, in coqrel.LogicalRelationsTests]
RemoveAllParams [record, in coqrel.Monotonicity]
RemoveParams [record, in coqrel.Monotonicity]
remove_all_params_candidate [instance, in coqrel.Monotonicity]
remove_params_candidate [instance, in coqrel.Monotonicity]
req [inductive, in coqrel.RelOperators]
req_corefl [lemma, in coqrel.RelOperators]
req_rintro [lemma, in coqrel.RelOperators]
req_intro [constructor, in coqrel.RelOperators]
respectful_relim [lemma, in coqrel.MorphismsInterop]
respectful_rintro [lemma, in coqrel.MorphismsInterop]
respectful_params [instance, in coqrel.MorphismsInterop]
respectful_subrel [instance, in coqrel.MorphismsInterop]
rexists [projection, in coqrel.RelDefinitions]
RExists [record, in coqrel.RelDefinitions]
rexists [constructor, in coqrel.RelDefinitions]
RExists [inductive, in coqrel.RelDefinitions]
rexists_rstep [instance, in coqrel.RelDefinitions]
rgraph_queue_cons [constructor, in coqrel.PreOrderTactic]
rgraph_queue_nil [constructor, in coqrel.PreOrderTactic]
rgraph_queue [inductive, in coqrel.PreOrderTactic]
rgraph_done [definition, in coqrel.PreOrderTactic]
Rg:139 [binder, in coqrel.Monotonicity]
right_le [constructor, in coqrel.BoolRel]
right_rel [instance, in coqrel.BoolRel]
right_rel_def [constructor, in coqrel.BoolRel]
rimpl [projection, in coqrel.Monotonicity]
RImpl [record, in coqrel.Monotonicity]
rimpl [constructor, in coqrel.Monotonicity]
RImpl [inductive, in coqrel.Monotonicity]
rimpl_flip_subrel [instance, in coqrel.Monotonicity]
rimpl_subrel [instance, in coqrel.Monotonicity]
rimpl_refl [instance, in coqrel.Monotonicity]
rintro [projection, in coqrel.RelDefinitions]
RIntro [record, in coqrel.RelDefinitions]
rintro [constructor, in coqrel.RelDefinitions]
RIntro [inductive, in coqrel.RelDefinitions]
rintro_rstep [instance, in coqrel.RelDefinitions]
RR:46 [binder, in coqrel.KLR]
RR:51 [binder, in coqrel.KLR]
RR:56 [binder, in coqrel.KLR]
RR:63 [binder, in coqrel.KLR]
RR:70 [binder, in coqrel.KLR]
RR:76 [binder, in coqrel.KLR]
RR:84 [binder, in coqrel.KLR]
rsat [definition, in coqrel.RelOperators]
rsat_subrel_params [instance, in coqrel.RelOperators]
rsat_subrel [instance, in coqrel.RelOperators]
rstep [projection, in coqrel.RelDefinitions]
RStep [record, in coqrel.RelDefinitions]
rstep [constructor, in coqrel.RelDefinitions]
RStep [inductive, in coqrel.RelDefinitions]
RW1:257 [binder, in coqrel.KLR]
RW2:258 [binder, in coqrel.KLR]
R':105 [binder, in coqrel.Monotonicity]
R':120 [binder, in coqrel.LogicalRelationsTests]
R':230 [binder, in coqrel.LogicalRelationsTests]
R':49 [binder, in coqrel.Monotonicity]
R':58 [binder, in coqrel.Monotonicity]
R':68 [binder, in coqrel.Monotonicity]
R':79 [binder, in coqrel.Monotonicity]
R':94 [binder, in coqrel.LogicalRelationsTests]
R':96 [binder, in coqrel.RelOperators]
R':99 [binder, in coqrel.Monotonicity]
R1':157 [binder, in coqrel.LogicalRelationsTests]
R1':189 [binder, in coqrel.LogicalRelationsTests]
R1':41 [binder, in coqrel.LogicalRelationsTests]
R12:231 [binder, in coqrel.RelOperators]
R13:233 [binder, in coqrel.RelOperators]
R1:101 [binder, in coqrel.RelDefinitions]
R1:107 [binder, in coqrel.RelOperators]
R1:11 [binder, in coqrel.RelOperators]
R1:111 [binder, in coqrel.RelDefinitions]
R1:113 [binder, in coqrel.RelOperators]
R1:119 [binder, in coqrel.RelOperators]
R1:123 [binder, in coqrel.LogicalRelationsTests]
R1:138 [binder, in coqrel.LogicalRelationsTests]
R1:14 [binder, in coqrel.Transport]
R1:155 [binder, in coqrel.LogicalRelationsTests]
R1:167 [binder, in coqrel.Relators]
R1:17 [binder, in coqrel.RelOperators]
R1:171 [binder, in coqrel.Relators]
R1:175 [binder, in coqrel.Relators]
R1:179 [binder, in coqrel.Relators]
R1:183 [binder, in coqrel.Relators]
R1:187 [binder, in coqrel.LogicalRelationsTests]
R1:215 [binder, in coqrel.LogicalRelationsTests]
R1:216 [binder, in coqrel.Relators]
R1:220 [binder, in coqrel.Relators]
R1:224 [binder, in coqrel.Relators]
R1:228 [binder, in coqrel.Relators]
R1:232 [binder, in coqrel.Relators]
R1:24 [binder, in coqrel.RelOperators]
R1:29 [binder, in coqrel.RelOperators]
R1:3 [binder, in coqrel.RelOperators]
R1:33 [binder, in coqrel.RelOperators]
R1:37 [binder, in coqrel.RelOperators]
R1:40 [binder, in coqrel.RelOperators]
R1:40 [binder, in coqrel.LogicalRelationsTests]
R1:43 [binder, in coqrel.RelOperators]
R1:46 [binder, in coqrel.RelOperators]
R1:47 [binder, in coqrel.KLR]
R1:50 [binder, in coqrel.RelOperators]
R1:52 [binder, in coqrel.KLR]
R1:57 [binder, in coqrel.KLR]
R1:58 [binder, in coqrel.RelOperators]
R1:61 [binder, in coqrel.MorphismsInterop]
R1:64 [binder, in coqrel.KLR]
R1:64 [binder, in coqrel.RelOperators]
R1:69 [binder, in coqrel.RelOperators]
R1:71 [binder, in coqrel.KLR]
R1:75 [binder, in coqrel.RelOperators]
R1:77 [binder, in coqrel.KLR]
R1:78 [binder, in coqrel.RelOperators]
R1:81 [binder, in coqrel.RelOperators]
R1:84 [binder, in coqrel.RelOperators]
R1:85 [binder, in coqrel.KLR]
R1:87 [binder, in coqrel.RelOperators]
R1:90 [binder, in coqrel.RelOperators]
R1:99 [binder, in coqrel.RelOperators]
R2':43 [binder, in coqrel.LogicalRelationsTests]
R23:232 [binder, in coqrel.RelOperators]
R2:100 [binder, in coqrel.RelOperators]
R2:102 [binder, in coqrel.RelDefinitions]
R2:108 [binder, in coqrel.RelOperators]
R2:112 [binder, in coqrel.RelDefinitions]
R2:114 [binder, in coqrel.RelOperators]
R2:12 [binder, in coqrel.RelOperators]
R2:120 [binder, in coqrel.RelOperators]
R2:124 [binder, in coqrel.LogicalRelationsTests]
R2:139 [binder, in coqrel.LogicalRelationsTests]
R2:15 [binder, in coqrel.Transport]
R2:156 [binder, in coqrel.LogicalRelationsTests]
R2:168 [binder, in coqrel.Relators]
R2:172 [binder, in coqrel.Relators]
R2:176 [binder, in coqrel.Relators]
R2:18 [binder, in coqrel.RelOperators]
R2:180 [binder, in coqrel.Relators]
R2:184 [binder, in coqrel.Relators]
R2:188 [binder, in coqrel.LogicalRelationsTests]
R2:216 [binder, in coqrel.LogicalRelationsTests]
R2:217 [binder, in coqrel.Relators]
R2:221 [binder, in coqrel.Relators]
R2:225 [binder, in coqrel.Relators]
R2:229 [binder, in coqrel.Relators]
R2:233 [binder, in coqrel.Relators]
R2:25 [binder, in coqrel.RelOperators]
R2:30 [binder, in coqrel.RelOperators]
R2:34 [binder, in coqrel.RelOperators]
R2:38 [binder, in coqrel.RelOperators]
R2:4 [binder, in coqrel.RelOperators]
R2:41 [binder, in coqrel.RelOperators]
R2:42 [binder, in coqrel.LogicalRelationsTests]
R2:44 [binder, in coqrel.RelOperators]
R2:47 [binder, in coqrel.RelOperators]
R2:51 [binder, in coqrel.RelOperators]
R2:59 [binder, in coqrel.RelOperators]
R2:62 [binder, in coqrel.MorphismsInterop]
R2:65 [binder, in coqrel.KLR]
R2:65 [binder, in coqrel.RelOperators]
R2:70 [binder, in coqrel.RelOperators]
R2:72 [binder, in coqrel.KLR]
R2:76 [binder, in coqrel.RelOperators]
R2:78 [binder, in coqrel.KLR]
R2:79 [binder, in coqrel.RelOperators]
R2:82 [binder, in coqrel.RelOperators]
R2:85 [binder, in coqrel.RelOperators]
R2:86 [binder, in coqrel.KLR]
R2:88 [binder, in coqrel.RelOperators]
R2:91 [binder, in coqrel.RelOperators]
R3:217 [binder, in coqrel.LogicalRelationsTests]
R:102 [binder, in coqrel.Relators]
R:102 [binder, in coqrel.LogicalRelationsTests]
R:104 [binder, in coqrel.Monotonicity]
R:108 [binder, in coqrel.RelDefinitions]
R:108 [binder, in coqrel.LogicalRelationsTests]
R:11 [binder, in coqrel.OptionRel]
R:110 [binder, in coqrel.KLR]
R:111 [binder, in coqrel.Relators]
R:112 [binder, in coqrel.LogicalRelationsTests]
R:114 [binder, in coqrel.Monotonicity]
R:116 [binder, in coqrel.LogicalRelationsTests]
R:118 [binder, in coqrel.KLR]
R:119 [binder, in coqrel.Relators]
R:119 [binder, in coqrel.LogicalRelationsTests]
R:123 [binder, in coqrel.Monotonicity]
R:127 [binder, in coqrel.RelOperators]
R:128 [binder, in coqrel.LogicalRelationsTests]
R:129 [binder, in coqrel.Relators]
R:13 [binder, in coqrel.RelQuotient]
R:134 [binder, in coqrel.Monotonicity]
R:137 [binder, in coqrel.Relators]
R:14 [binder, in coqrel.OptionRel]
R:14 [binder, in coqrel.Relators]
R:14 [binder, in coqrel.RDestruct]
R:140 [binder, in coqrel.LogicalRelationsTests]
R:143 [binder, in coqrel.KLR]
R:152 [binder, in coqrel.Monotonicity]
R:153 [binder, in coqrel.KLR]
R:158 [binder, in coqrel.LogicalRelationsTests]
R:162 [binder, in coqrel.KLR]
R:164 [binder, in coqrel.RelOperators]
R:167 [binder, in coqrel.RelOperators]
R:17 [binder, in coqrel.LogicalRelationsTests]
R:172 [binder, in coqrel.KLR]
R:18 [binder, in coqrel.RelQuotient]
R:182 [binder, in coqrel.KLR]
R:190 [binder, in coqrel.KLR]
R:190 [binder, in coqrel.LogicalRelationsTests]
R:194 [binder, in coqrel.LogicalRelationsTests]
R:196 [binder, in coqrel.RelDefinitions]
R:2 [binder, in coqrel.RelClasses]
R:2 [binder, in coqrel.RelQuotient]
R:20 [binder, in coqrel.RelQuotient]
R:203 [binder, in coqrel.KLR]
R:205 [binder, in coqrel.RelOperators]
R:206 [binder, in coqrel.LogicalRelationsTests]
R:208 [binder, in coqrel.RelDefinitions]
R:21 [binder, in coqrel.OptionRel]
R:21 [binder, in coqrel.Relators]
R:212 [binder, in coqrel.KLR]
R:213 [binder, in coqrel.RelDefinitions]
R:217 [binder, in coqrel.RelOperators]
R:22 [binder, in coqrel.RelClasses]
R:22 [binder, in coqrel.RelQuotient]
R:220 [binder, in coqrel.RelDefinitions]
R:221 [binder, in coqrel.RelOperators]
R:225 [binder, in coqrel.RelDefinitions]
R:226 [binder, in coqrel.KLR]
R:229 [binder, in coqrel.RelDefinitions]
R:229 [binder, in coqrel.LogicalRelationsTests]
R:23 [binder, in coqrel.OptionRel]
R:23 [binder, in coqrel.RelOperators]
R:234 [binder, in coqrel.KLR]
R:234 [binder, in coqrel.RelDefinitions]
R:238 [binder, in coqrel.LogicalRelationsTests]
R:24 [binder, in coqrel.Transport]
R:240 [binder, in coqrel.KLR]
R:240 [binder, in coqrel.RelOperators]
R:241 [binder, in coqrel.Relators]
R:242 [binder, in coqrel.Relators]
R:244 [binder, in coqrel.LogicalRelationsTests]
R:249 [binder, in coqrel.RelOperators]
R:251 [binder, in coqrel.KLR]
R:252 [binder, in coqrel.Relators]
R:259 [binder, in coqrel.Relators]
R:26 [binder, in coqrel.MorphismsInterop]
R:260 [binder, in coqrel.RelOperators]
R:262 [binder, in coqrel.Relators]
R:263 [binder, in coqrel.Relators]
R:264 [binder, in coqrel.KLR]
R:273 [binder, in coqrel.KLR]
R:274 [binder, in coqrel.RelOperators]
R:278 [binder, in coqrel.Relators]
R:279 [binder, in coqrel.Relators]
R:28 [binder, in coqrel.RelOperators]
R:283 [binder, in coqrel.RelOperators]
R:292 [binder, in coqrel.RelOperators]
R:3 [binder, in coqrel.Transport]
R:3 [binder, in coqrel.PreOrderTactic]
R:31 [binder, in coqrel.LogicalRelationsTests]
R:311 [binder, in coqrel.RelOperators]
R:318 [binder, in coqrel.RelOperators]
R:33 [binder, in coqrel.Transport]
R:33 [binder, in coqrel.KLR]
R:33 [binder, in coqrel.RelDefinitions]
R:33 [binder, in coqrel.MorphismsInterop]
R:330 [binder, in coqrel.RelOperators]
R:35 [binder, in coqrel.RelOperators]
R:36 [binder, in coqrel.OptionRel]
R:36 [binder, in coqrel.KLR]
R:369 [binder, in coqrel.RelOperators]
R:378 [binder, in coqrel.RelOperators]
R:38 [binder, in coqrel.RelDefinitions]
R:385 [binder, in coqrel.RelOperators]
R:39 [binder, in coqrel.OptionRel]
R:394 [binder, in coqrel.RelOperators]
R:40 [binder, in coqrel.KLR]
R:403 [binder, in coqrel.RelOperators]
R:410 [binder, in coqrel.RelOperators]
R:420 [binder, in coqrel.RelOperators]
R:43 [binder, in coqrel.MorphismsInterop]
R:433 [binder, in coqrel.RelOperators]
R:442 [binder, in coqrel.RelOperators]
R:46 [binder, in coqrel.Transport]
R:46 [binder, in coqrel.OptionRel]
R:46 [binder, in coqrel.LogicalRelationsTests]
R:48 [binder, in coqrel.OptionRel]
R:49 [binder, in coqrel.MorphismsInterop]
R:53 [binder, in coqrel.OptionRel]
R:53 [binder, in coqrel.RelDefinitions]
R:57 [binder, in coqrel.Monotonicity]
R:58 [binder, in coqrel.MorphismsInterop]
R:60 [binder, in coqrel.OptionRel]
R:61 [binder, in coqrel.RelDefinitions]
R:63 [binder, in coqrel.Relators]
R:65 [binder, in coqrel.Monotonicity]
R:66 [binder, in coqrel.RelDefinitions]
R:66 [binder, in coqrel.RelOperators]
R:7 [binder, in coqrel.PreOrderTactic]
R:71 [binder, in coqrel.RelOperators]
R:74 [binder, in coqrel.RelOperators]
R:75 [binder, in coqrel.RelDefinitions]
R:76 [binder, in coqrel.Monotonicity]
R:78 [binder, in coqrel.LogicalRelationsTests]
R:80 [binder, in coqrel.RelDefinitions]
R:84 [binder, in coqrel.Monotonicity]
R:86 [binder, in coqrel.LogicalRelationsTests]
R:9 [binder, in coqrel.RelClasses]
R:9 [binder, in coqrel.RelQuotient]
R:91 [binder, in coqrel.RelDefinitions]
R:93 [binder, in coqrel.RelOperators]
R:93 [binder, in coqrel.Monotonicity]
R:93 [binder, in coqrel.LogicalRelationsTests]
R:95 [binder, in coqrel.RelOperators]
R:96 [binder, in coqrel.RelDefinitions]
R:98 [binder, in coqrel.Monotonicity]
S
sA:112 [binder, in coqrel.Relators]sA:112 [binder, in coqrel.KLR]
sA:120 [binder, in coqrel.KLR]
sA:130 [binder, in coqrel.Relators]
sA:25 [binder, in coqrel.Transport]
sA:34 [binder, in coqrel.Transport]
sA:47 [binder, in coqrel.Transport]
sB:113 [binder, in coqrel.Relators]
sB:113 [binder, in coqrel.KLR]
sB:121 [binder, in coqrel.KLR]
sB:131 [binder, in coqrel.Relators]
sB:26 [binder, in coqrel.Transport]
sB:35 [binder, in coqrel.Transport]
sB:48 [binder, in coqrel.Transport]
set_le_transport [lemma, in coqrel.Transport]
set_ge_compose [instance, in coqrel.Relators]
set_ge_refl [lemma, in coqrel.Relators]
set_ge_subrel_params [instance, in coqrel.Relators]
set_ge_subrel [instance, in coqrel.Relators]
set_ge [definition, in coqrel.Relators]
set_le_compose [instance, in coqrel.Relators]
set_le_refl [lemma, in coqrel.Relators]
set_le_subrel_params [instance, in coqrel.Relators]
set_le_subrel [instance, in coqrel.Relators]
set_le [definition, in coqrel.Relators]
set_kge [definition, in coqrel.KLR]
set_kle [definition, in coqrel.KLR]
snd_rel [instance, in coqrel.Relators]
Some_ge [instance, in coqrel.OptionRel]
Some_ge_def [constructor, in coqrel.OptionRel]
Some_le [instance, in coqrel.OptionRel]
Some_le_def [constructor, in coqrel.OptionRel]
Some_rel [instance, in coqrel.Relators]
Some_rel_def [constructor, in coqrel.Relators]
subrel [definition, in coqrel.RelDefinitions]
subrelation_subrel [lemma, in coqrel.MorphismsInterop]
SubrelMonotonicity [record, in coqrel.Monotonicity]
SubrelMonotonicity [inductive, in coqrel.Monotonicity]
subrel_eq [instance, in coqrel.RelClasses]
subrel_impl_relim [instance, in coqrel.RelDefinitions]
subrel_preorder [instance, in coqrel.RelDefinitions]
subrel_sym_flip [lemma, in coqrel.RelOperators]
subrel_monotonicity [projection, in coqrel.Monotonicity]
subrel_monotonicity [constructor, in coqrel.Monotonicity]
sumbool_le [inductive, in coqrel.BoolRel]
sumbool_rel [inductive, in coqrel.BoolRel]
sum_rel_preorder [lemma, in coqrel.Relators]
sum_rel_sym [lemma, in coqrel.Relators]
sum_rel_trans [lemma, in coqrel.Relators]
sum_rel_corefl [lemma, in coqrel.Relators]
sum_rel_refl [lemma, in coqrel.Relators]
sum_subrel_params [instance, in coqrel.Relators]
sum_subrel [instance, in coqrel.Relators]
sum_rel [inductive, in coqrel.Relators]
sum_klr [definition, in coqrel.KLR]
S:195 [binder, in coqrel.LogicalRelationsTests]
S:95 [binder, in coqrel.LogicalRelationsTests]
T
transitive_rcompose [lemma, in coqrel.RelClasses]transport [projection, in coqrel.Transport]
Transport [record, in coqrel.Transport]
transport [constructor, in coqrel.Transport]
Transport [inductive, in coqrel.Transport]
Transport [library]
transport_in_goal [lemma, in coqrel.Transport]
true_leb [lemma, in coqrel.BoolRel]
tt_rel [constructor, in coqrel.Relators]
Tw:446 [binder, in coqrel.RelOperators]
T:196 [binder, in coqrel.LogicalRelationsTests]
t:203 [binder, in coqrel.LogicalRelationsTests]
T:221 [binder, in coqrel.RelDefinitions]
t:27 [binder, in coqrel.LogicalRelationsTests]
T:28 [binder, in coqrel.Relators]
T:32 [binder, in coqrel.Relators]
T:444 [binder, in coqrel.RelOperators]
T:81 [binder, in coqrel.RelDefinitions]
U
unconvertible [projection, in coqrel.RelDefinitions]Unconvertible [record, in coqrel.RelDefinitions]
unconvertible [constructor, in coqrel.RelDefinitions]
Unconvertible [inductive, in coqrel.RelDefinitions]
Unconvertible0:66 [binder, in coqrel.Transport]
uncurry [definition, in coqrel.RelOperators]
UnfoldUncurry [record, in coqrel.RelOperators]
UnfoldUncurry [inductive, in coqrel.RelOperators]
unfold_monotonic_rstep [lemma, in coqrel.RelDefinitions]
unfold_uncurry_before_after [projection, in coqrel.RelOperators]
unfold_uncurry_before_after [constructor, in coqrel.RelOperators]
unit_rel [inductive, in coqrel.Relators]
UNKRIPKIFY [section, in coqrel.KLR]
Unnamed_thm26 [definition, in coqrel.LogicalRelationsTests]
Unnamed_thm25 [definition, in coqrel.LogicalRelationsTests]
Unnamed_thm24 [definition, in coqrel.LogicalRelationsTests]
Unnamed_thm24 [definition, in coqrel.LogicalRelationsTests]
Unnamed_thm23 [definition, in coqrel.LogicalRelationsTests]
Unnamed_thm22 [definition, in coqrel.LogicalRelationsTests]
Unnamed_thm21 [definition, in coqrel.LogicalRelationsTests]
Unnamed_thm20 [definition, in coqrel.LogicalRelationsTests]
Unnamed_thm19 [definition, in coqrel.LogicalRelationsTests]
Unnamed_thm18 [definition, in coqrel.LogicalRelationsTests]
Unnamed_thm17 [definition, in coqrel.LogicalRelationsTests]
Unnamed_thm16 [definition, in coqrel.LogicalRelationsTests]
Unnamed_thm15 [definition, in coqrel.LogicalRelationsTests]
Unnamed_thm14 [definition, in coqrel.LogicalRelationsTests]
Unnamed_thm13 [definition, in coqrel.LogicalRelationsTests]
Unnamed_thm13 [definition, in coqrel.LogicalRelationsTests]
Unnamed_thm12 [definition, in coqrel.LogicalRelationsTests]
Unnamed_thm11 [definition, in coqrel.LogicalRelationsTests]
Unnamed_thm11 [definition, in coqrel.LogicalRelationsTests]
Unnamed_thm10 [definition, in coqrel.LogicalRelationsTests]
Unnamed_thm9 [definition, in coqrel.LogicalRelationsTests]
Unnamed_thm8 [definition, in coqrel.LogicalRelationsTests]
Unnamed_thm7 [definition, in coqrel.LogicalRelationsTests]
Unnamed_thm7 [definition, in coqrel.LogicalRelationsTests]
Unnamed_thm6 [definition, in coqrel.LogicalRelationsTests]
Unnamed_thm5 [definition, in coqrel.LogicalRelationsTests]
Unnamed_thm4 [definition, in coqrel.LogicalRelationsTests]
Unnamed_thm3 [definition, in coqrel.LogicalRelationsTests]
Unnamed_thm2 [definition, in coqrel.LogicalRelationsTests]
Unnamed_thm1 [definition, in coqrel.LogicalRelationsTests]
Unnamed_thm0 [definition, in coqrel.LogicalRelationsTests]
Unnamed_thm [definition, in coqrel.LogicalRelationsTests]
Unnamed_thm [definition, in coqrel.LogicalRelationsTests]
USUAL [section, in coqrel.KLR]
u:11 [binder, in coqrel.RelQuotient]
u:16 [binder, in coqrel.RelQuotient]
u:188 [binder, in coqrel.RelDefinitions]
V
var1:49 [binder, in coqrel.KLR]var1:67 [binder, in coqrel.KLR]
var2:68 [binder, in coqrel.KLR]
var:35 [binder, in coqrel.KLR]
var:50 [binder, in coqrel.KLR]
var:69 [binder, in coqrel.KLR]
v1:105 [binder, in coqrel.Relators]
V1:155 [binder, in coqrel.RelDefinitions]
v1:160 [binder, in coqrel.RelDefinitions]
v1:162 [binder, in coqrel.RelDefinitions]
v1:167 [binder, in coqrel.RelDefinitions]
v1:170 [binder, in coqrel.RelDefinitions]
v1:173 [binder, in coqrel.RelDefinitions]
V1:178 [binder, in coqrel.RelDefinitions]
V1:191 [binder, in coqrel.RelDefinitions]
v1:199 [binder, in coqrel.RelDefinitions]
V1:69 [binder, in coqrel.Relators]
v1:74 [binder, in coqrel.Relators]
v1:76 [binder, in coqrel.Relators]
v1:81 [binder, in coqrel.Relators]
v1:83 [binder, in coqrel.Relators]
V1:85 [binder, in coqrel.Relators]
v1:90 [binder, in coqrel.Relators]
v1:95 [binder, in coqrel.Relators]
V1:97 [binder, in coqrel.Relators]
v2:106 [binder, in coqrel.Relators]
V2:156 [binder, in coqrel.RelDefinitions]
v2:161 [binder, in coqrel.RelDefinitions]
v2:163 [binder, in coqrel.RelDefinitions]
v2:168 [binder, in coqrel.RelDefinitions]
v2:171 [binder, in coqrel.RelDefinitions]
v2:174 [binder, in coqrel.RelDefinitions]
V2:179 [binder, in coqrel.RelDefinitions]
V2:192 [binder, in coqrel.RelDefinitions]
v2:200 [binder, in coqrel.RelDefinitions]
V2:70 [binder, in coqrel.Relators]
v2:75 [binder, in coqrel.Relators]
v2:77 [binder, in coqrel.Relators]
v2:82 [binder, in coqrel.Relators]
v2:84 [binder, in coqrel.Relators]
V2:86 [binder, in coqrel.Relators]
v2:91 [binder, in coqrel.Relators]
v2:96 [binder, in coqrel.Relators]
V2:98 [binder, in coqrel.Relators]
v:189 [binder, in coqrel.RelDefinitions]
V:40 [binder, in coqrel.Relators]
v:43 [binder, in coqrel.Relators]
v:44 [binder, in coqrel.Relators]
v:45 [binder, in coqrel.Relators]
v:49 [binder, in coqrel.Relators]
v:50 [binder, in coqrel.Relators]
v:51 [binder, in coqrel.Relators]
V:52 [binder, in coqrel.Relators]
v:55 [binder, in coqrel.Relators]
v:59 [binder, in coqrel.Relators]
V:60 [binder, in coqrel.Relators]
v:66 [binder, in coqrel.Relators]
W
WA:8 [binder, in coqrel.KLR]WB:11 [binder, in coqrel.KLR]
w':147 [binder, in coqrel.KLR]
w':157 [binder, in coqrel.KLR]
w':164 [binder, in coqrel.KLR]
w':176 [binder, in coqrel.KLR]
w':184 [binder, in coqrel.KLR]
w':196 [binder, in coqrel.KLR]
w':209 [binder, in coqrel.KLR]
w':220 [binder, in coqrel.KLR]
w':424 [binder, in coqrel.RelOperators]
w':435 [binder, in coqrel.RelOperators]
w':448 [binder, in coqrel.RelOperators]
W1:246 [binder, in coqrel.KLR]
W1:253 [binder, in coqrel.KLR]
W1:259 [binder, in coqrel.KLR]
W1:268 [binder, in coqrel.KLR]
W2:247 [binder, in coqrel.KLR]
W2:254 [binder, in coqrel.KLR]
W2:260 [binder, in coqrel.KLR]
W2:269 [binder, in coqrel.KLR]
W:1 [binder, in coqrel.KLR]
w:111 [binder, in coqrel.KLR]
w:119 [binder, in coqrel.KLR]
W:124 [binder, in coqrel.KLR]
W:127 [binder, in coqrel.KLR]
W:130 [binder, in coqrel.KLR]
w:144 [binder, in coqrel.KLR]
w:154 [binder, in coqrel.KLR]
w:163 [binder, in coqrel.KLR]
w:173 [binder, in coqrel.KLR]
w:18 [binder, in coqrel.KLR]
w:183 [binder, in coqrel.KLR]
w:191 [binder, in coqrel.KLR]
W:197 [binder, in coqrel.KLR]
w:204 [binder, in coqrel.KLR]
w:21 [binder, in coqrel.KLR]
W:210 [binder, in coqrel.LogicalRelationsTests]
w:213 [binder, in coqrel.KLR]
w:223 [binder, in coqrel.LogicalRelationsTests]
w:224 [binder, in coqrel.LogicalRelationsTests]
w:225 [binder, in coqrel.LogicalRelationsTests]
w:229 [binder, in coqrel.KLR]
w:237 [binder, in coqrel.KLR]
w:241 [binder, in coqrel.KLR]
w:252 [binder, in coqrel.KLR]
w:265 [binder, in coqrel.KLR]
w:274 [binder, in coqrel.KLR]
w:34 [binder, in coqrel.KLR]
w:37 [binder, in coqrel.KLR]
w:41 [binder, in coqrel.KLR]
W:416 [binder, in coqrel.RelOperators]
w:421 [binder, in coqrel.RelOperators]
W:425 [binder, in coqrel.RelOperators]
W:429 [binder, in coqrel.RelOperators]
w:434 [binder, in coqrel.RelOperators]
W:438 [binder, in coqrel.RelOperators]
w:443 [binder, in coqrel.RelOperators]
w:445 [binder, in coqrel.RelOperators]
w:48 [binder, in coqrel.KLR]
W:5 [binder, in coqrel.KLR]
w:53 [binder, in coqrel.KLR]
w:58 [binder, in coqrel.KLR]
w:66 [binder, in coqrel.KLR]
w:73 [binder, in coqrel.KLR]
w:79 [binder, in coqrel.KLR]
w:87 [binder, in coqrel.KLR]
X
xa1:163 [binder, in coqrel.LogicalRelationsTests]xa2:164 [binder, in coqrel.LogicalRelationsTests]
xb1:167 [binder, in coqrel.LogicalRelationsTests]
xb2:168 [binder, in coqrel.LogicalRelationsTests]
x1:113 [binder, in coqrel.RelDefinitions]
x1:145 [binder, in coqrel.LogicalRelationsTests]
x1:191 [binder, in coqrel.Relators]
x1:279 [binder, in coqrel.RelOperators]
x1:288 [binder, in coqrel.RelOperators]
x1:97 [binder, in coqrel.LogicalRelationsTests]
x2:114 [binder, in coqrel.RelDefinitions]
x2:146 [binder, in coqrel.LogicalRelationsTests]
x2:192 [binder, in coqrel.Relators]
x2:280 [binder, in coqrel.RelOperators]
x2:289 [binder, in coqrel.RelOperators]
x2:99 [binder, in coqrel.LogicalRelationsTests]
x:1 [binder, in coqrel.RDestruct]
x:101 [binder, in coqrel.RelOperators]
x:103 [binder, in coqrel.RelDefinitions]
x:105 [binder, in coqrel.LogicalRelationsTests]
x:106 [binder, in coqrel.Monotonicity]
x:109 [binder, in coqrel.RelOperators]
x:109 [binder, in coqrel.LogicalRelationsTests]
x:11 [binder, in coqrel.PreOrderTactic]
x:11 [binder, in coqrel.RelDefinitions]
x:113 [binder, in coqrel.LogicalRelationsTests]
x:115 [binder, in coqrel.RelOperators]
x:123 [binder, in coqrel.RelOperators]
x:127 [binder, in coqrel.RelDefinitions]
x:13 [binder, in coqrel.PreOrderTactic]
x:13 [binder, in coqrel.RelOperators]
x:130 [binder, in coqrel.RelOperators]
x:135 [binder, in coqrel.RelOperators]
x:139 [binder, in coqrel.RelOperators]
x:14 [binder, in coqrel.RelQuotient]
x:140 [binder, in coqrel.Monotonicity]
x:141 [binder, in coqrel.RelDefinitions]
x:141 [binder, in coqrel.LogicalRelationsTests]
x:145 [binder, in coqrel.KLR]
x:15 [binder, in coqrel.PreOrderTactic]
x:153 [binder, in coqrel.RelOperators]
x:155 [binder, in coqrel.KLR]
x:159 [binder, in coqrel.LogicalRelationsTests]
x:16 [binder, in coqrel.Transport]
x:165 [binder, in coqrel.KLR]
x:17 [binder, in coqrel.Relators]
x:17 [binder, in coqrel.RelClasses]
x:174 [binder, in coqrel.KLR]
x:183 [binder, in coqrel.RelDefinitions]
x:185 [binder, in coqrel.KLR]
x:19 [binder, in coqrel.RelOperators]
x:191 [binder, in coqrel.LogicalRelationsTests]
x:192 [binder, in coqrel.KLR]
x:2 [binder, in coqrel.RelDefinitions]
x:200 [binder, in coqrel.LogicalRelationsTests]
x:206 [binder, in coqrel.RelOperators]
X:209 [binder, in coqrel.LogicalRelationsTests]
x:22 [binder, in coqrel.BoolRel]
x:222 [binder, in coqrel.LogicalRelationsTests]
x:227 [binder, in coqrel.KLR]
x:23 [binder, in coqrel.RelQuotient]
x:23 [binder, in coqrel.LogicalRelationsTests]
x:233 [binder, in coqrel.LogicalRelationsTests]
x:235 [binder, in coqrel.KLR]
x:239 [binder, in coqrel.LogicalRelationsTests]
x:24 [binder, in coqrel.RDestruct]
x:241 [binder, in coqrel.RelOperators]
x:242 [binder, in coqrel.KLR]
x:246 [binder, in coqrel.LogicalRelationsTests]
x:249 [binder, in coqrel.LogicalRelationsTests]
x:250 [binder, in coqrel.RelOperators]
x:253 [binder, in coqrel.Relators]
x:253 [binder, in coqrel.LogicalRelationsTests]
x:256 [binder, in coqrel.LogicalRelationsTests]
x:258 [binder, in coqrel.LogicalRelationsTests]
x:26 [binder, in coqrel.Monotonicity]
x:263 [binder, in coqrel.RelOperators]
x:266 [binder, in coqrel.KLR]
x:27 [binder, in coqrel.Monotonicity]
x:275 [binder, in coqrel.KLR]
x:28 [binder, in coqrel.RelQuotient]
x:31 [binder, in coqrel.OptionRel]
x:31 [binder, in coqrel.RDestruct]
x:33 [binder, in coqrel.OptionRel]
x:33 [binder, in coqrel.RelClasses]
x:33 [binder, in coqrel.LogicalRelationsTests]
x:34 [binder, in coqrel.RelDefinitions]
x:347 [binder, in coqrel.RelOperators]
x:354 [binder, in coqrel.RelOperators]
x:360 [binder, in coqrel.RelOperators]
x:370 [binder, in coqrel.RelOperators]
x:373 [binder, in coqrel.RelOperators]
x:38 [binder, in coqrel.KLR]
x:386 [binder, in coqrel.RelOperators]
x:395 [binder, in coqrel.RelOperators]
x:398 [binder, in coqrel.RelOperators]
x:4 [binder, in coqrel.RelClasses]
x:40 [binder, in coqrel.OptionRel]
x:411 [binder, in coqrel.RelOperators]
x:42 [binder, in coqrel.KLR]
x:49 [binder, in coqrel.LogicalRelationsTests]
x:5 [binder, in coqrel.RelOperators]
x:52 [binder, in coqrel.RelOperators]
x:54 [binder, in coqrel.OptionRel]
x:54 [binder, in coqrel.KLR]
x:58 [binder, in coqrel.LogicalRelationsTests]
x:59 [binder, in coqrel.KLR]
x:6 [binder, in coqrel.OptionRel]
x:6 [binder, in coqrel.RelQuotient]
x:60 [binder, in coqrel.RelOperators]
x:61 [binder, in coqrel.OptionRel]
x:63 [binder, in coqrel.LogicalRelationsTests]
x:70 [binder, in coqrel.LogicalRelationsTests]
x:74 [binder, in coqrel.KLR]
x:8 [binder, in coqrel.RDestruct]
x:80 [binder, in coqrel.KLR]
x:80 [binder, in coqrel.LogicalRelationsTests]
x:83 [binder, in coqrel.LogicalRelationsTests]
x:85 [binder, in coqrel.Monotonicity]
x:88 [binder, in coqrel.LogicalRelationsTests]
x:9 [binder, in coqrel.MorphismsInterop]
Y
ya1:165 [binder, in coqrel.LogicalRelationsTests]ya2:166 [binder, in coqrel.LogicalRelationsTests]
yb1:169 [binder, in coqrel.LogicalRelationsTests]
yb2:170 [binder, in coqrel.LogicalRelationsTests]
y1:115 [binder, in coqrel.RelDefinitions]
y1:147 [binder, in coqrel.LogicalRelationsTests]
y1:281 [binder, in coqrel.RelOperators]
y1:290 [binder, in coqrel.RelOperators]
y1:98 [binder, in coqrel.LogicalRelationsTests]
y2:100 [binder, in coqrel.LogicalRelationsTests]
y2:116 [binder, in coqrel.RelDefinitions]
y2:148 [binder, in coqrel.LogicalRelationsTests]
y2:282 [binder, in coqrel.RelOperators]
y2:291 [binder, in coqrel.RelOperators]
y:10 [binder, in coqrel.MorphismsInterop]
y:102 [binder, in coqrel.RelOperators]
y:104 [binder, in coqrel.RelDefinitions]
y:106 [binder, in coqrel.LogicalRelationsTests]
y:107 [binder, in coqrel.Monotonicity]
y:110 [binder, in coqrel.RelOperators]
y:110 [binder, in coqrel.LogicalRelationsTests]
y:114 [binder, in coqrel.LogicalRelationsTests]
y:116 [binder, in coqrel.RelOperators]
y:12 [binder, in coqrel.PreOrderTactic]
y:12 [binder, in coqrel.RelDefinitions]
y:124 [binder, in coqrel.RelOperators]
y:128 [binder, in coqrel.RelDefinitions]
y:131 [binder, in coqrel.RelOperators]
y:136 [binder, in coqrel.RelOperators]
y:14 [binder, in coqrel.RelOperators]
y:140 [binder, in coqrel.RelOperators]
y:141 [binder, in coqrel.Monotonicity]
y:142 [binder, in coqrel.RelDefinitions]
y:142 [binder, in coqrel.LogicalRelationsTests]
y:146 [binder, in coqrel.KLR]
y:15 [binder, in coqrel.OptionRel]
y:15 [binder, in coqrel.RelQuotient]
y:155 [binder, in coqrel.RelOperators]
y:156 [binder, in coqrel.KLR]
y:160 [binder, in coqrel.LogicalRelationsTests]
y:166 [binder, in coqrel.KLR]
y:17 [binder, in coqrel.Transport]
y:175 [binder, in coqrel.KLR]
y:18 [binder, in coqrel.RelClasses]
y:184 [binder, in coqrel.RelDefinitions]
y:186 [binder, in coqrel.KLR]
y:192 [binder, in coqrel.LogicalRelationsTests]
y:193 [binder, in coqrel.KLR]
y:2 [binder, in coqrel.RDestruct]
y:20 [binder, in coqrel.RelOperators]
y:201 [binder, in coqrel.LogicalRelationsTests]
y:207 [binder, in coqrel.RelOperators]
y:226 [binder, in coqrel.LogicalRelationsTests]
y:228 [binder, in coqrel.KLR]
y:23 [binder, in coqrel.BoolRel]
y:234 [binder, in coqrel.LogicalRelationsTests]
y:236 [binder, in coqrel.KLR]
y:24 [binder, in coqrel.LogicalRelationsTests]
y:240 [binder, in coqrel.LogicalRelationsTests]
y:242 [binder, in coqrel.RelOperators]
y:243 [binder, in coqrel.KLR]
y:247 [binder, in coqrel.LogicalRelationsTests]
y:25 [binder, in coqrel.RDestruct]
y:251 [binder, in coqrel.RelOperators]
y:254 [binder, in coqrel.Relators]
y:259 [binder, in coqrel.LogicalRelationsTests]
y:264 [binder, in coqrel.RelOperators]
y:267 [binder, in coqrel.KLR]
y:276 [binder, in coqrel.KLR]
y:29 [binder, in coqrel.RelQuotient]
y:32 [binder, in coqrel.OptionRel]
y:32 [binder, in coqrel.RDestruct]
y:34 [binder, in coqrel.LogicalRelationsTests]
y:348 [binder, in coqrel.RelOperators]
y:35 [binder, in coqrel.RelClasses]
y:355 [binder, in coqrel.RelOperators]
y:371 [binder, in coqrel.RelOperators]
y:374 [binder, in coqrel.RelOperators]
y:387 [binder, in coqrel.RelOperators]
y:39 [binder, in coqrel.KLR]
y:396 [binder, in coqrel.RelOperators]
y:399 [binder, in coqrel.RelOperators]
y:412 [binder, in coqrel.RelOperators]
y:43 [binder, in coqrel.KLR]
y:5 [binder, in coqrel.RelClasses]
y:50 [binder, in coqrel.LogicalRelationsTests]
y:53 [binder, in coqrel.RelOperators]
y:55 [binder, in coqrel.OptionRel]
y:55 [binder, in coqrel.KLR]
y:6 [binder, in coqrel.RelOperators]
y:60 [binder, in coqrel.KLR]
y:61 [binder, in coqrel.RelOperators]
y:62 [binder, in coqrel.OptionRel]
y:64 [binder, in coqrel.LogicalRelationsTests]
y:7 [binder, in coqrel.OptionRel]
y:71 [binder, in coqrel.LogicalRelationsTests]
y:75 [binder, in coqrel.KLR]
y:8 [binder, in coqrel.OptionRel]
y:81 [binder, in coqrel.KLR]
y:81 [binder, in coqrel.LogicalRelationsTests]
y:84 [binder, in coqrel.LogicalRelationsTests]
y:86 [binder, in coqrel.Monotonicity]
y:89 [binder, in coqrel.LogicalRelationsTests]
y:9 [binder, in coqrel.RDestruct]
Z
z:154 [binder, in coqrel.RelOperators]z:19 [binder, in coqrel.RelClasses]
z:202 [binder, in coqrel.LogicalRelationsTests]
z:26 [binder, in coqrel.LogicalRelationsTests]
z:260 [binder, in coqrel.LogicalRelationsTests]
z:34 [binder, in coqrel.RelClasses]
z:72 [binder, in coqrel.LogicalRelationsTests]
other
_ @@ [ _ ] (klr_scope) [notation, in coqrel.KLR]<> * _ (klr_scope) [notation, in coqrel.KLR]
[] -> _ (klr_scope) [notation, in coqrel.KLR]
<> _ (klr_scope) [notation, in coqrel.KLR]
[] _ (klr_scope) [notation, in coqrel.KLR]
< _ > _ (klr_scope) [notation, in coqrel.KLR]
[ _ ] _ (klr_scope) [notation, in coqrel.KLR]
% _ (klr_scope) [notation, in coqrel.KLR]
_ /\ _ (klr_scope) [notation, in coqrel.KLR]
_ \/ _ (klr_scope) [notation, in coqrel.KLR]
_ + _ (klr_scope) [notation, in coqrel.KLR]
_ * _ (klr_scope) [notation, in coqrel.KLR]
- ==> _ (klr_scope) [notation, in coqrel.KLR]
_ --> _ (klr_scope) [notation, in coqrel.KLR]
_ ++> _ (klr_scope) [notation, in coqrel.KLR]
_ ==> _ (klr_scope) [notation, in coqrel.KLR]
_ * _ (rel_scope) [notation, in coqrel.Relators]
_ + _ (rel_scope) [notation, in coqrel.Relators]
forallr _ _ : _ , _ (rel_scope) [notation, in coqrel.Relators]
- ==> _ (rel_scope) [notation, in coqrel.Relators]
|= _ (rel_scope) [notation, in coqrel.KLR]
forallr _ , _ (rel_scope) [notation, in coqrel.RelDefinitions]
forallr _ : _ , _ (rel_scope) [notation, in coqrel.RelDefinitions]
forallr _ @ _ _ , _ (rel_scope) [notation, in coqrel.RelDefinitions]
forallr _ @ _ _ : _ , _ (rel_scope) [notation, in coqrel.RelDefinitions]
_ --> _ (rel_scope) [notation, in coqrel.RelDefinitions]
_ ++> _ (rel_scope) [notation, in coqrel.RelDefinitions]
_ ==> _ (rel_scope) [notation, in coqrel.RelDefinitions]
rexists _ .. _ , _ (rel_scope) [notation, in coqrel.RelOperators]
rforall _ .. _ , _ (rel_scope) [notation, in coqrel.RelOperators]
% _ (rel_scope) [notation, in coqrel.RelOperators]
_ !! ( _ ) (rel_scope) [notation, in coqrel.RelOperators]
_ !! _ (rel_scope) [notation, in coqrel.RelOperators]
_ !! ( _ , _ ) (rel_scope) [notation, in coqrel.RelOperators]
_ @@ ( _ ) (rel_scope) [notation, in coqrel.RelOperators]
_ @@ _ (rel_scope) [notation, in coqrel.RelOperators]
_ @@ ( _ , _ ) (rel_scope) [notation, in coqrel.RelOperators]
⊤ (rel_scope) [notation, in coqrel.RelOperators]
⊥ (rel_scope) [notation, in coqrel.RelOperators]
_ /\ _ (rel_scope) [notation, in coqrel.RelOperators]
_ \/ _ (rel_scope) [notation, in coqrel.RelOperators]
_ ~> _ [notation, in coqrel.KLR]
forallr - , _ [notation, in coqrel.Relators]
forallr - : _ , _ [notation, in coqrel.Relators]
forallr - @ _ , _ [notation, in coqrel.Relators]
forallr - @ _ : _ , _ [notation, in coqrel.Relators]
@ Monotonic _ _ _ [notation, in coqrel.RelDefinitions]
Notation Index
other
_ @@ [ _ ] (klr_scope) [in coqrel.KLR]<> * _ (klr_scope) [in coqrel.KLR]
[] -> _ (klr_scope) [in coqrel.KLR]
<> _ (klr_scope) [in coqrel.KLR]
[] _ (klr_scope) [in coqrel.KLR]
< _ > _ (klr_scope) [in coqrel.KLR]
[ _ ] _ (klr_scope) [in coqrel.KLR]
% _ (klr_scope) [in coqrel.KLR]
_ /\ _ (klr_scope) [in coqrel.KLR]
_ \/ _ (klr_scope) [in coqrel.KLR]
_ + _ (klr_scope) [in coqrel.KLR]
_ * _ (klr_scope) [in coqrel.KLR]
- ==> _ (klr_scope) [in coqrel.KLR]
_ --> _ (klr_scope) [in coqrel.KLR]
_ ++> _ (klr_scope) [in coqrel.KLR]
_ ==> _ (klr_scope) [in coqrel.KLR]
_ * _ (rel_scope) [in coqrel.Relators]
_ + _ (rel_scope) [in coqrel.Relators]
forallr _ _ : _ , _ (rel_scope) [in coqrel.Relators]
- ==> _ (rel_scope) [in coqrel.Relators]
|= _ (rel_scope) [in coqrel.KLR]
forallr _ , _ (rel_scope) [in coqrel.RelDefinitions]
forallr _ : _ , _ (rel_scope) [in coqrel.RelDefinitions]
forallr _ @ _ _ , _ (rel_scope) [in coqrel.RelDefinitions]
forallr _ @ _ _ : _ , _ (rel_scope) [in coqrel.RelDefinitions]
_ --> _ (rel_scope) [in coqrel.RelDefinitions]
_ ++> _ (rel_scope) [in coqrel.RelDefinitions]
_ ==> _ (rel_scope) [in coqrel.RelDefinitions]
rexists _ .. _ , _ (rel_scope) [in coqrel.RelOperators]
rforall _ .. _ , _ (rel_scope) [in coqrel.RelOperators]
% _ (rel_scope) [in coqrel.RelOperators]
_ !! ( _ ) (rel_scope) [in coqrel.RelOperators]
_ !! _ (rel_scope) [in coqrel.RelOperators]
_ !! ( _ , _ ) (rel_scope) [in coqrel.RelOperators]
_ @@ ( _ ) (rel_scope) [in coqrel.RelOperators]
_ @@ _ (rel_scope) [in coqrel.RelOperators]
_ @@ ( _ , _ ) (rel_scope) [in coqrel.RelOperators]
⊤ (rel_scope) [in coqrel.RelOperators]
⊥ (rel_scope) [in coqrel.RelOperators]
_ /\ _ (rel_scope) [in coqrel.RelOperators]
_ \/ _ (rel_scope) [in coqrel.RelOperators]
_ ~> _ [in coqrel.KLR]
forallr - , _ [in coqrel.Relators]
forallr - : _ , _ [in coqrel.Relators]
forallr - @ _ , _ [in coqrel.Relators]
forallr - @ _ : _ , _ [in coqrel.Relators]
@ Monotonic _ _ _ [in coqrel.RelDefinitions]
Binder Index
A
ab:303 [in coqrel.RelOperators]acc:211 [in coqrel.LogicalRelationsTests]
acc:419 [in coqrel.RelOperators]
acc:428 [in coqrel.RelOperators]
acc:432 [in coqrel.RelOperators]
acc:441 [in coqrel.RelOperators]
after:321 [in coqrel.RelOperators]
A':201 [in coqrel.RelOperators]
A':210 [in coqrel.RelOperators]
A':236 [in coqrel.RelOperators]
A':245 [in coqrel.RelOperators]
A1:1 [in coqrel.OptionRel]
A1:10 [in coqrel.Transport]
A1:102 [in coqrel.KLR]
A1:106 [in coqrel.KLR]
A1:119 [in coqrel.RelDefinitions]
A1:129 [in coqrel.RelDefinitions]
a1:130 [in coqrel.LogicalRelationsTests]
A1:131 [in coqrel.KLR]
A1:133 [in coqrel.RelDefinitions]
A1:134 [in coqrel.LogicalRelationsTests]
A1:143 [in coqrel.RelDefinitions]
A1:149 [in coqrel.Relators]
A1:149 [in coqrel.LogicalRelationsTests]
A1:161 [in coqrel.Relators]
a1:18 [in coqrel.Transport]
A1:18 [in coqrel.RelDefinitions]
A1:181 [in coqrel.LogicalRelationsTests]
A1:185 [in coqrel.Relators]
a1:19 [in coqrel.KLR]
A1:199 [in coqrel.Relators]
A1:203 [in coqrel.Relators]
a1:210 [in coqrel.Relators]
A1:222 [in coqrel.RelOperators]
A1:234 [in coqrel.Relators]
A1:239 [in coqrel.Relators]
A1:243 [in coqrel.Relators]
A1:254 [in coqrel.RelOperators]
A1:257 [in coqrel.Relators]
A1:26 [in coqrel.OptionRel]
A1:264 [in coqrel.Relators]
A1:265 [in coqrel.RelOperators]
A1:27 [in coqrel.KLR]
A1:275 [in coqrel.RelOperators]
A1:284 [in coqrel.RelOperators]
A1:29 [in coqrel.Transport]
A1:305 [in coqrel.RelOperators]
A1:312 [in coqrel.RelOperators]
A1:324 [in coqrel.RelOperators]
A1:34 [in coqrel.OptionRel]
a1:36 [in coqrel.Transport]
A1:36 [in coqrel.LogicalRelationsTests]
A1:40 [in coqrel.Transport]
A1:45 [in coqrel.RelClasses]
a1:49 [in coqrel.Transport]
A1:9 [in coqrel.OptionRel]
A1:9 [in coqrel.KLR]
A1:91 [in coqrel.KLR]
A1:98 [in coqrel.KLR]
A2:10 [in coqrel.OptionRel]
A2:10 [in coqrel.KLR]
A2:103 [in coqrel.KLR]
A2:107 [in coqrel.KLR]
A2:12 [in coqrel.Transport]
A2:120 [in coqrel.RelDefinitions]
A2:130 [in coqrel.RelDefinitions]
a2:131 [in coqrel.LogicalRelationsTests]
A2:134 [in coqrel.KLR]
A2:134 [in coqrel.RelDefinitions]
A2:135 [in coqrel.LogicalRelationsTests]
A2:144 [in coqrel.RelDefinitions]
A2:150 [in coqrel.Relators]
A2:150 [in coqrel.LogicalRelationsTests]
A2:162 [in coqrel.Relators]
A2:182 [in coqrel.LogicalRelationsTests]
A2:186 [in coqrel.Relators]
a2:19 [in coqrel.Transport]
A2:19 [in coqrel.RelDefinitions]
A2:2 [in coqrel.OptionRel]
a2:20 [in coqrel.KLR]
A2:200 [in coqrel.Relators]
A2:205 [in coqrel.Relators]
a2:211 [in coqrel.Relators]
A2:223 [in coqrel.RelOperators]
A2:235 [in coqrel.Relators]
A2:240 [in coqrel.Relators]
A2:244 [in coqrel.Relators]
A2:255 [in coqrel.RelOperators]
A2:258 [in coqrel.Relators]
A2:265 [in coqrel.Relators]
A2:266 [in coqrel.RelOperators]
A2:27 [in coqrel.OptionRel]
A2:276 [in coqrel.RelOperators]
A2:285 [in coqrel.RelOperators]
A2:29 [in coqrel.KLR]
A2:30 [in coqrel.Transport]
A2:308 [in coqrel.RelOperators]
A2:315 [in coqrel.RelOperators]
A2:327 [in coqrel.RelOperators]
A2:35 [in coqrel.OptionRel]
a2:37 [in coqrel.Transport]
A2:37 [in coqrel.LogicalRelationsTests]
A2:41 [in coqrel.Transport]
A2:46 [in coqrel.RelClasses]
a2:50 [in coqrel.Transport]
A2:92 [in coqrel.KLR]
A2:99 [in coqrel.KLR]
A3:224 [in coqrel.RelOperators]
A3:42 [in coqrel.Transport]
A3:47 [in coqrel.RelClasses]
a3:51 [in coqrel.Transport]
A:1 [in coqrel.Transport]
A:1 [in coqrel.PreOrderTactic]
A:1 [in coqrel.Relators]
A:1 [in coqrel.RelClasses]
A:1 [in coqrel.RelDefinitions]
A:1 [in coqrel.RelOperators]
A:1 [in coqrel.RelQuotient]
A:1 [in coqrel.Monotonicity]
A:1 [in coqrel.MorphismsInterop]
A:10 [in coqrel.RelClasses]
A:10 [in coqrel.RDestruct]
A:10 [in coqrel.RelDefinitions]
a:10 [in coqrel.RelQuotient]
A:101 [in coqrel.LogicalRelationsTests]
A:102 [in coqrel.Monotonicity]
A:103 [in coqrel.RelOperators]
A:105 [in coqrel.RelDefinitions]
A:105 [in coqrel.RelOperators]
A:107 [in coqrel.RelDefinitions]
A:107 [in coqrel.LogicalRelationsTests]
A:108 [in coqrel.KLR]
A:109 [in coqrel.Relators]
A:109 [in coqrel.RelDefinitions]
A:11 [in coqrel.Relators]
A:11 [in coqrel.MorphismsInterop]
A:111 [in coqrel.RelOperators]
A:111 [in coqrel.LogicalRelationsTests]
A:112 [in coqrel.Monotonicity]
a:114 [in coqrel.Relators]
a:114 [in coqrel.KLR]
A:115 [in coqrel.LogicalRelationsTests]
A:116 [in coqrel.Relators]
A:116 [in coqrel.KLR]
A:117 [in coqrel.RelOperators]
A:118 [in coqrel.Relators]
A:118 [in coqrel.LogicalRelationsTests]
A:12 [in coqrel.OptionRel]
A:12 [in coqrel.RelQuotient]
A:120 [in coqrel.Monotonicity]
A:121 [in coqrel.RelOperators]
A:122 [in coqrel.LogicalRelationsTests]
a:123 [in coqrel.KLR]
A:125 [in coqrel.KLR]
A:125 [in coqrel.RelOperators]
A:125 [in coqrel.LogicalRelationsTests]
A:127 [in coqrel.Relators]
A:128 [in coqrel.KLR]
A:128 [in coqrel.RelOperators]
A:130 [in coqrel.Monotonicity]
a:133 [in coqrel.Relators]
A:133 [in coqrel.RelOperators]
A:134 [in coqrel.Relators]
A:136 [in coqrel.Relators]
A:137 [in coqrel.RelOperators]
A:14 [in coqrel.LogicalRelationsTests]
A:140 [in coqrel.KLR]
A:141 [in coqrel.RelOperators]
A:142 [in coqrel.RelOperators]
A:142 [in coqrel.Monotonicity]
A:143 [in coqrel.LogicalRelationsTests]
A:144 [in coqrel.RelOperators]
A:146 [in coqrel.RelOperators]
A:148 [in coqrel.KLR]
A:148 [in coqrel.RelOperators]
A:149 [in coqrel.Monotonicity]
A:15 [in coqrel.RelOperators]
A:15 [in coqrel.Monotonicity]
a:15 [in coqrel.LogicalRelationsTests]
A:150 [in coqrel.KLR]
A:156 [in coqrel.RelOperators]
A:156 [in coqrel.Monotonicity]
A:159 [in coqrel.KLR]
A:159 [in coqrel.RelOperators]
A:16 [in coqrel.OptionRel]
A:161 [in coqrel.LogicalRelationsTests]
A:162 [in coqrel.RelOperators]
A:165 [in coqrel.Relators]
A:165 [in coqrel.RelOperators]
A:168 [in coqrel.RelOperators]
A:169 [in coqrel.Relators]
A:169 [in coqrel.KLR]
A:17 [in coqrel.RelQuotient]
A:173 [in coqrel.Relators]
A:175 [in coqrel.RelOperators]
A:177 [in coqrel.Relators]
A:177 [in coqrel.KLR]
A:179 [in coqrel.KLR]
A:18 [in coqrel.OptionRel]
A:18 [in coqrel.Relators]
A:180 [in coqrel.RelOperators]
A:181 [in coqrel.Relators]
A:187 [in coqrel.KLR]
A:19 [in coqrel.RDestruct]
A:19 [in coqrel.RelQuotient]
A:193 [in coqrel.LogicalRelationsTests]
A:199 [in coqrel.RelOperators]
A:2 [in coqrel.KLR]
A:20 [in coqrel.OptionRel]
A:20 [in coqrel.LogicalRelationsTests]
A:201 [in coqrel.KLR]
A:204 [in coqrel.RelDefinitions]
A:204 [in coqrel.LogicalRelationsTests]
A:206 [in coqrel.RelDefinitions]
A:208 [in coqrel.RelOperators]
A:21 [in coqrel.RelClasses]
A:21 [in coqrel.RelOperators]
A:21 [in coqrel.RelQuotient]
A:21 [in coqrel.MorphismsInterop]
A:210 [in coqrel.KLR]
A:211 [in coqrel.RelDefinitions]
A:212 [in coqrel.LogicalRelationsTests]
A:214 [in coqrel.Relators]
a:214 [in coqrel.KLR]
A:214 [in coqrel.RelOperators]
A:218 [in coqrel.Relators]
A:218 [in coqrel.RelDefinitions]
A:218 [in coqrel.RelOperators]
A:22 [in coqrel.Transport]
A:22 [in coqrel.OptionRel]
a:220 [in coqrel.LogicalRelationsTests]
A:222 [in coqrel.Relators]
A:223 [in coqrel.RelDefinitions]
A:224 [in coqrel.KLR]
A:226 [in coqrel.Relators]
A:227 [in coqrel.RelDefinitions]
A:227 [in coqrel.LogicalRelationsTests]
A:23 [in coqrel.MorphismsInterop]
A:230 [in coqrel.Relators]
A:230 [in coqrel.KLR]
A:232 [in coqrel.KLR]
A:232 [in coqrel.RelDefinitions]
A:234 [in coqrel.RelOperators]
A:235 [in coqrel.LogicalRelationsTests]
A:238 [in coqrel.KLR]
a:24 [in coqrel.RelQuotient]
A:241 [in coqrel.LogicalRelationsTests]
A:243 [in coqrel.RelOperators]
A:248 [in coqrel.KLR]
A:248 [in coqrel.LogicalRelationsTests]
a:25 [in coqrel.MorphismsInterop]
A:250 [in coqrel.Relators]
a:250 [in coqrel.LogicalRelationsTests]
a:251 [in coqrel.LogicalRelationsTests]
A:252 [in coqrel.LogicalRelationsTests]
a:254 [in coqrel.LogicalRelationsTests]
a:255 [in coqrel.Relators]
A:255 [in coqrel.KLR]
A:255 [in coqrel.LogicalRelationsTests]
A:257 [in coqrel.LogicalRelationsTests]
A:26 [in coqrel.RelClasses]
A:26 [in coqrel.RDestruct]
A:26 [in coqrel.RelOperators]
A:261 [in coqrel.KLR]
a:27 [in coqrel.Transport]
A:270 [in coqrel.KLR]
A:271 [in coqrel.RelOperators]
A:28 [in coqrel.Monotonicity]
A:28 [in coqrel.LogicalRelationsTests]
A:286 [in coqrel.Relators]
A:288 [in coqrel.Relators]
A:289 [in coqrel.Relators]
a:29 [in coqrel.LogicalRelationsTests]
a:29 [in coqrel.MorphismsInterop]
A:293 [in coqrel.RelOperators]
a:297 [in coqrel.RelOperators]
A:299 [in coqrel.RelOperators]
A:3 [in coqrel.RDestruct]
A:3 [in coqrel.LogicalRelationsTests]
A:3 [in coqrel.MorphismsInterop]
A:30 [in coqrel.MorphismsInterop]
A:31 [in coqrel.KLR]
A:31 [in coqrel.RelOperators]
A:319 [in coqrel.RelOperators]
A:32 [in coqrel.RelDefinitions]
a:32 [in coqrel.MorphismsInterop]
A:336 [in coqrel.RelOperators]
a:337 [in coqrel.RelOperators]
A:340 [in coqrel.RelOperators]
a:341 [in coqrel.RelOperators]
A:342 [in coqrel.RelOperators]
a:343 [in coqrel.RelOperators]
A:344 [in coqrel.RelOperators]
A:349 [in coqrel.RelOperators]
A:35 [in coqrel.RelDefinitions]
A:351 [in coqrel.RelOperators]
A:356 [in coqrel.RelOperators]
A:358 [in coqrel.RelOperators]
A:36 [in coqrel.RelOperators]
a:36 [in coqrel.MorphismsInterop]
A:363 [in coqrel.RelOperators]
A:364 [in coqrel.RelOperators]
A:366 [in coqrel.RelOperators]
A:37 [in coqrel.OptionRel]
A:37 [in coqrel.RelClasses]
A:375 [in coqrel.RelOperators]
A:38 [in coqrel.Monotonicity]
A:382 [in coqrel.RelOperators]
A:39 [in coqrel.RelOperators]
A:39 [in coqrel.MorphismsInterop]
A:391 [in coqrel.RelOperators]
a:4 [in coqrel.Transport]
a:4 [in coqrel.PreOrderTactic]
A:4 [in coqrel.RelDefinitions]
a:4 [in coqrel.LogicalRelationsTests]
A:400 [in coqrel.RelOperators]
A:407 [in coqrel.RelOperators]
A:41 [in coqrel.OptionRel]
A:41 [in coqrel.RelClasses]
A:41 [in coqrel.MorphismsInterop]
A:417 [in coqrel.RelOperators]
A:42 [in coqrel.RelOperators]
a:422 [in coqrel.RelOperators]
A:426 [in coqrel.RelOperators]
A:43 [in coqrel.OptionRel]
A:430 [in coqrel.RelOperators]
A:439 [in coqrel.RelOperators]
A:44 [in coqrel.LogicalRelationsTests]
A:45 [in coqrel.OptionRel]
A:45 [in coqrel.RelOperators]
a:46 [in coqrel.MorphismsInterop]
A:47 [in coqrel.OptionRel]
A:47 [in coqrel.Monotonicity]
A:47 [in coqrel.MorphismsInterop]
A:48 [in coqrel.RelOperators]
a:5 [in coqrel.RelQuotient]
A:5 [in coqrel.LogicalRelationsTests]
A:50 [in coqrel.RelDefinitions]
A:51 [in coqrel.OptionRel]
A:52 [in coqrel.LogicalRelationsTests]
a:52 [in coqrel.MorphismsInterop]
A:54 [in coqrel.RelOperators]
A:55 [in coqrel.Monotonicity]
A:55 [in coqrel.MorphismsInterop]
a:56 [in coqrel.OptionRel]
A:56 [in coqrel.RelOperators]
A:57 [in coqrel.MorphismsInterop]
A:58 [in coqrel.OptionRel]
A:58 [in coqrel.RelDefinitions]
A:59 [in coqrel.LogicalRelationsTests]
a:59 [in coqrel.MorphismsInterop]
A:6 [in coqrel.PreOrderTactic]
a:6 [in coqrel.RelDefinitions]
a:6 [in coqrel.LogicalRelationsTests]
A:60 [in coqrel.MorphismsInterop]
A:61 [in coqrel.Monotonicity]
A:62 [in coqrel.RelOperators]
A:64 [in coqrel.RelDefinitions]
A:66 [in coqrel.LogicalRelationsTests]
A:67 [in coqrel.RelOperators]
a:7 [in coqrel.Relators]
A:7 [in coqrel.RelClasses]
A:7 [in coqrel.RelOperators]
A:7 [in coqrel.Monotonicity]
A:72 [in coqrel.RelOperators]
A:72 [in coqrel.Monotonicity]
A:73 [in coqrel.RelDefinitions]
a:73 [in coqrel.LogicalRelationsTests]
a:75 [in coqrel.LogicalRelationsTests]
A:77 [in coqrel.RelOperators]
A:77 [in coqrel.LogicalRelationsTests]
A:78 [in coqrel.RelDefinitions]
A:8 [in coqrel.Relators]
A:8 [in coqrel.RelClasses]
A:8 [in coqrel.RelQuotient]
A:8 [in coqrel.LogicalRelationsTests]
A:80 [in coqrel.RelOperators]
A:82 [in coqrel.Monotonicity]
A:83 [in coqrel.RelOperators]
A:85 [in coqrel.LogicalRelationsTests]
A:86 [in coqrel.RelOperators]
A:87 [in coqrel.RelDefinitions]
A:89 [in coqrel.RelOperators]
A:9 [in coqrel.RelOperators]
a:9 [in coqrel.LogicalRelationsTests]
A:90 [in coqrel.LogicalRelationsTests]
A:91 [in coqrel.Monotonicity]
A:92 [in coqrel.RelOperators]
A:94 [in coqrel.RelDefinitions]
A:94 [in coqrel.RelOperators]
A:95 [in coqrel.KLR]
A:96 [in coqrel.Monotonicity]
A:97 [in coqrel.RelOperators]
A:99 [in coqrel.RelDefinitions]
B
before:320 [in coqrel.RelOperators]B':202 [in coqrel.RelOperators]
B':211 [in coqrel.RelOperators]
B':237 [in coqrel.RelOperators]
B':246 [in coqrel.RelOperators]
B1:100 [in coqrel.KLR]
B1:104 [in coqrel.KLR]
B1:11 [in coqrel.Transport]
B1:12 [in coqrel.Relators]
B1:12 [in coqrel.KLR]
B1:121 [in coqrel.RelDefinitions]
B1:131 [in coqrel.RelDefinitions]
B1:132 [in coqrel.KLR]
B1:135 [in coqrel.RelDefinitions]
B1:136 [in coqrel.LogicalRelationsTests]
B1:145 [in coqrel.RelDefinitions]
B1:151 [in coqrel.Relators]
B1:151 [in coqrel.LogicalRelationsTests]
B1:163 [in coqrel.Relators]
b1:17 [in coqrel.BoolRel]
B1:183 [in coqrel.LogicalRelationsTests]
B1:187 [in coqrel.Relators]
B1:19 [in coqrel.Relators]
B1:2 [in coqrel.Relators]
b1:20 [in coqrel.Transport]
B1:201 [in coqrel.Relators]
B1:204 [in coqrel.Relators]
b1:212 [in coqrel.Relators]
b1:22 [in coqrel.KLR]
B1:225 [in coqrel.RelOperators]
B1:256 [in coqrel.RelOperators]
B1:267 [in coqrel.RelOperators]
B1:277 [in coqrel.RelOperators]
B1:28 [in coqrel.KLR]
B1:286 [in coqrel.RelOperators]
B1:306 [in coqrel.RelOperators]
B1:31 [in coqrel.Transport]
B1:313 [in coqrel.RelOperators]
B1:325 [in coqrel.RelOperators]
b1:38 [in coqrel.Transport]
B1:38 [in coqrel.LogicalRelationsTests]
B1:43 [in coqrel.Transport]
B1:51 [in coqrel.RelClasses]
b1:52 [in coqrel.Transport]
B1:9 [in coqrel.Relators]
B1:93 [in coqrel.KLR]
B1:96 [in coqrel.KLR]
B2:10 [in coqrel.Relators]
B2:101 [in coqrel.KLR]
B2:105 [in coqrel.KLR]
B2:122 [in coqrel.RelDefinitions]
B2:13 [in coqrel.Transport]
B2:13 [in coqrel.Relators]
B2:13 [in coqrel.KLR]
B2:132 [in coqrel.RelDefinitions]
B2:135 [in coqrel.KLR]
B2:136 [in coqrel.RelDefinitions]
B2:137 [in coqrel.LogicalRelationsTests]
B2:146 [in coqrel.RelDefinitions]
B2:152 [in coqrel.Relators]
B2:152 [in coqrel.LogicalRelationsTests]
B2:164 [in coqrel.Relators]
B2:184 [in coqrel.LogicalRelationsTests]
B2:188 [in coqrel.Relators]
B2:20 [in coqrel.Relators]
b2:20 [in coqrel.BoolRel]
B2:202 [in coqrel.Relators]
B2:206 [in coqrel.Relators]
b2:21 [in coqrel.Transport]
b2:213 [in coqrel.Relators]
B2:226 [in coqrel.RelOperators]
b2:23 [in coqrel.KLR]
B2:257 [in coqrel.RelOperators]
B2:268 [in coqrel.RelOperators]
B2:278 [in coqrel.RelOperators]
B2:287 [in coqrel.RelOperators]
B2:3 [in coqrel.Relators]
B2:30 [in coqrel.KLR]
B2:309 [in coqrel.RelOperators]
B2:316 [in coqrel.RelOperators]
B2:32 [in coqrel.Transport]
B2:328 [in coqrel.RelOperators]
b2:39 [in coqrel.Transport]
B2:39 [in coqrel.LogicalRelationsTests]
B2:44 [in coqrel.Transport]
B2:52 [in coqrel.RelClasses]
b2:53 [in coqrel.Transport]
B2:94 [in coqrel.KLR]
B2:97 [in coqrel.KLR]
B3:227 [in coqrel.RelOperators]
B3:45 [in coqrel.Transport]
B3:53 [in coqrel.RelClasses]
b3:54 [in coqrel.Transport]
B:10 [in coqrel.RelOperators]
b:10 [in coqrel.LogicalRelationsTests]
B:100 [in coqrel.RelDefinitions]
B:103 [in coqrel.Monotonicity]
B:104 [in coqrel.RelOperators]
B:106 [in coqrel.RelDefinitions]
B:106 [in coqrel.RelOperators]
B:109 [in coqrel.KLR]
B:11 [in coqrel.RelClasses]
B:11 [in coqrel.RDestruct]
B:110 [in coqrel.Relators]
B:110 [in coqrel.RelDefinitions]
B:112 [in coqrel.RelOperators]
B:113 [in coqrel.Monotonicity]
b:115 [in coqrel.Relators]
b:115 [in coqrel.KLR]
B:117 [in coqrel.Relators]
B:117 [in coqrel.KLR]
B:118 [in coqrel.RelOperators]
B:12 [in coqrel.MorphismsInterop]
B:121 [in coqrel.Monotonicity]
b:122 [in coqrel.KLR]
B:122 [in coqrel.RelOperators]
B:126 [in coqrel.KLR]
B:126 [in coqrel.RelOperators]
B:126 [in coqrel.LogicalRelationsTests]
B:128 [in coqrel.Relators]
B:129 [in coqrel.KLR]
B:129 [in coqrel.RelOperators]
B:13 [in coqrel.OptionRel]
B:131 [in coqrel.Monotonicity]
b:132 [in coqrel.Relators]
b:132 [in coqrel.LogicalRelationsTests]
B:134 [in coqrel.RelOperators]
B:135 [in coqrel.Relators]
B:138 [in coqrel.RelOperators]
B:141 [in coqrel.KLR]
B:143 [in coqrel.RelOperators]
B:143 [in coqrel.Monotonicity]
B:144 [in coqrel.LogicalRelationsTests]
B:145 [in coqrel.RelOperators]
B:147 [in coqrel.RelOperators]
B:149 [in coqrel.KLR]
B:149 [in coqrel.RelOperators]
B:150 [in coqrel.Monotonicity]
B:151 [in coqrel.KLR]
B:157 [in coqrel.RelOperators]
B:157 [in coqrel.Monotonicity]
B:16 [in coqrel.RelOperators]
B:16 [in coqrel.Monotonicity]
b:16 [in coqrel.LogicalRelationsTests]
B:160 [in coqrel.KLR]
B:160 [in coqrel.RelOperators]
B:162 [in coqrel.LogicalRelationsTests]
B:163 [in coqrel.RelOperators]
B:166 [in coqrel.Relators]
B:166 [in coqrel.RelOperators]
B:169 [in coqrel.RelOperators]
B:17 [in coqrel.OptionRel]
B:170 [in coqrel.Relators]
B:170 [in coqrel.KLR]
B:174 [in coqrel.Relators]
B:176 [in coqrel.RelOperators]
B:178 [in coqrel.Relators]
B:178 [in coqrel.KLR]
B:180 [in coqrel.KLR]
B:181 [in coqrel.RelOperators]
B:182 [in coqrel.Relators]
B:188 [in coqrel.KLR]
B:19 [in coqrel.OptionRel]
B:2 [in coqrel.Transport]
B:2 [in coqrel.PreOrderTactic]
B:2 [in coqrel.RelOperators]
B:2 [in coqrel.Monotonicity]
B:2 [in coqrel.MorphismsInterop]
B:20 [in coqrel.RDestruct]
B:200 [in coqrel.RelOperators]
B:202 [in coqrel.KLR]
B:205 [in coqrel.RelDefinitions]
B:205 [in coqrel.LogicalRelationsTests]
B:207 [in coqrel.RelDefinitions]
B:209 [in coqrel.RelOperators]
B:21 [in coqrel.LogicalRelationsTests]
B:211 [in coqrel.KLR]
B:212 [in coqrel.RelDefinitions]
B:213 [in coqrel.LogicalRelationsTests]
B:215 [in coqrel.Relators]
B:215 [in coqrel.RelOperators]
b:217 [in coqrel.KLR]
B:219 [in coqrel.Relators]
B:219 [in coqrel.RelDefinitions]
B:219 [in coqrel.RelOperators]
B:22 [in coqrel.RelOperators]
b:221 [in coqrel.LogicalRelationsTests]
B:223 [in coqrel.Relators]
B:224 [in coqrel.RelDefinitions]
B:225 [in coqrel.KLR]
B:227 [in coqrel.Relators]
B:228 [in coqrel.RelDefinitions]
B:228 [in coqrel.LogicalRelationsTests]
B:23 [in coqrel.Transport]
B:231 [in coqrel.Relators]
B:231 [in coqrel.KLR]
B:233 [in coqrel.KLR]
B:233 [in coqrel.RelDefinitions]
B:235 [in coqrel.RelOperators]
B:236 [in coqrel.LogicalRelationsTests]
B:239 [in coqrel.KLR]
B:24 [in coqrel.MorphismsInterop]
b:24 [in coqrel.BoolRel]
B:242 [in coqrel.LogicalRelationsTests]
B:244 [in coqrel.RelOperators]
B:249 [in coqrel.KLR]
b:25 [in coqrel.BoolRel]
B:251 [in coqrel.Relators]
b:256 [in coqrel.Relators]
B:256 [in coqrel.KLR]
B:262 [in coqrel.KLR]
B:27 [in coqrel.RelClasses]
B:27 [in coqrel.RDestruct]
B:27 [in coqrel.RelOperators]
B:271 [in coqrel.KLR]
B:272 [in coqrel.RelOperators]
b:28 [in coqrel.Transport]
B:287 [in coqrel.Relators]
B:29 [in coqrel.Monotonicity]
B:294 [in coqrel.RelOperators]
b:298 [in coqrel.RelOperators]
B:3 [in coqrel.KLR]
b:30 [in coqrel.LogicalRelationsTests]
B:300 [in coqrel.RelOperators]
B:31 [in coqrel.MorphismsInterop]
B:32 [in coqrel.KLR]
B:32 [in coqrel.RelOperators]
B:345 [in coqrel.RelOperators]
B:350 [in coqrel.RelOperators]
B:352 [in coqrel.RelOperators]
B:357 [in coqrel.RelOperators]
B:36 [in coqrel.RelDefinitions]
B:367 [in coqrel.RelOperators]
B:376 [in coqrel.RelOperators]
B:38 [in coqrel.OptionRel]
B:38 [in coqrel.RelClasses]
B:383 [in coqrel.RelOperators]
B:39 [in coqrel.Monotonicity]
B:392 [in coqrel.RelOperators]
B:4 [in coqrel.RDestruct]
B:4 [in coqrel.MorphismsInterop]
B:40 [in coqrel.MorphismsInterop]
B:401 [in coqrel.RelOperators]
B:408 [in coqrel.RelOperators]
B:418 [in coqrel.RelOperators]
B:42 [in coqrel.OptionRel]
B:42 [in coqrel.RelClasses]
B:42 [in coqrel.MorphismsInterop]
b:423 [in coqrel.RelOperators]
B:427 [in coqrel.RelOperators]
B:431 [in coqrel.RelOperators]
B:44 [in coqrel.OptionRel]
B:440 [in coqrel.RelOperators]
B:45 [in coqrel.LogicalRelationsTests]
B:48 [in coqrel.Monotonicity]
B:48 [in coqrel.MorphismsInterop]
B:49 [in coqrel.RelOperators]
b:5 [in coqrel.Transport]
b:5 [in coqrel.PreOrderTactic]
B:5 [in coqrel.RelDefinitions]
B:51 [in coqrel.RelDefinitions]
B:52 [in coqrel.OptionRel]
B:53 [in coqrel.LogicalRelationsTests]
B:55 [in coqrel.RelOperators]
B:56 [in coqrel.Monotonicity]
B:56 [in coqrel.MorphismsInterop]
b:57 [in coqrel.OptionRel]
B:57 [in coqrel.RelOperators]
B:59 [in coqrel.OptionRel]
B:59 [in coqrel.RelDefinitions]
B:60 [in coqrel.LogicalRelationsTests]
B:62 [in coqrel.Monotonicity]
B:63 [in coqrel.RelOperators]
B:65 [in coqrel.RelDefinitions]
B:67 [in coqrel.LogicalRelationsTests]
B:68 [in coqrel.RelOperators]
b:7 [in coqrel.RelDefinitions]
b:7 [in coqrel.LogicalRelationsTests]
B:73 [in coqrel.RelOperators]
B:73 [in coqrel.Monotonicity]
B:74 [in coqrel.RelDefinitions]
b:74 [in coqrel.LogicalRelationsTests]
b:76 [in coqrel.LogicalRelationsTests]
B:79 [in coqrel.RelDefinitions]
b:79 [in coqrel.LogicalRelationsTests]
B:8 [in coqrel.RelOperators]
B:8 [in coqrel.Monotonicity]
b:82 [in coqrel.LogicalRelationsTests]
B:83 [in coqrel.Monotonicity]
b:87 [in coqrel.LogicalRelationsTests]
B:88 [in coqrel.RelDefinitions]
B:91 [in coqrel.LogicalRelationsTests]
B:92 [in coqrel.Monotonicity]
B:95 [in coqrel.RelDefinitions]
B:97 [in coqrel.Monotonicity]
B:98 [in coqrel.RelOperators]
C
C1:133 [in coqrel.KLR]C1:153 [in coqrel.LogicalRelationsTests]
C1:185 [in coqrel.LogicalRelationsTests]
C1:307 [in coqrel.RelOperators]
C1:314 [in coqrel.RelOperators]
C1:326 [in coqrel.RelOperators]
C2:136 [in coqrel.KLR]
C2:154 [in coqrel.LogicalRelationsTests]
C2:186 [in coqrel.LogicalRelationsTests]
C2:310 [in coqrel.RelOperators]
C2:317 [in coqrel.RelOperators]
C2:329 [in coqrel.RelOperators]
C:104 [in coqrel.LogicalRelationsTests]
C:12 [in coqrel.RelClasses]
C:127 [in coqrel.LogicalRelationsTests]
C:132 [in coqrel.Monotonicity]
c:133 [in coqrel.LogicalRelationsTests]
C:144 [in coqrel.Monotonicity]
C:150 [in coqrel.RelOperators]
C:151 [in coqrel.Monotonicity]
C:158 [in coqrel.RelOperators]
C:161 [in coqrel.RelOperators]
C:17 [in coqrel.Monotonicity]
C:170 [in coqrel.RelOperators]
C:177 [in coqrel.RelOperators]
C:182 [in coqrel.RelOperators]
C:214 [in coqrel.LogicalRelationsTests]
C:28 [in coqrel.RelClasses]
C:295 [in coqrel.RelOperators]
C:30 [in coqrel.Monotonicity]
C:301 [in coqrel.RelOperators]
C:368 [in coqrel.RelOperators]
c:372 [in coqrel.RelOperators]
C:377 [in coqrel.RelOperators]
c:381 [in coqrel.RelOperators]
C:384 [in coqrel.RelOperators]
c:390 [in coqrel.RelOperators]
C:393 [in coqrel.RelOperators]
c:397 [in coqrel.RelOperators]
C:40 [in coqrel.Monotonicity]
C:402 [in coqrel.RelOperators]
c:404 [in coqrel.RelOperators]
C:409 [in coqrel.RelOperators]
c:415 [in coqrel.RelOperators]
C:63 [in coqrel.Monotonicity]
C:74 [in coqrel.Monotonicity]
C:9 [in coqrel.Monotonicity]
C:92 [in coqrel.LogicalRelationsTests]
D
D:133 [in coqrel.Monotonicity]D:171 [in coqrel.RelOperators]
D:18 [in coqrel.Monotonicity]
D:31 [in coqrel.Monotonicity]
D:41 [in coqrel.Monotonicity]
D:64 [in coqrel.Monotonicity]
D:75 [in coqrel.Monotonicity]
E
E:157 [in coqrel.RelDefinitions]e:169 [in coqrel.RelDefinitions]
e:172 [in coqrel.RelDefinitions]
e:175 [in coqrel.RelDefinitions]
e:176 [in coqrel.RelDefinitions]
e:177 [in coqrel.RelDefinitions]
E:180 [in coqrel.RelDefinitions]
e:190 [in coqrel.RelDefinitions]
E:193 [in coqrel.RelDefinitions]
e:201 [in coqrel.RelDefinitions]
E:71 [in coqrel.Relators]
E:87 [in coqrel.Relators]
E:99 [in coqrel.Relators]
F
FE:164 [in coqrel.RelDefinitions]FE:185 [in coqrel.RelDefinitions]
FE:46 [in coqrel.Relators]
FE:56 [in coqrel.Relators]
FE:78 [in coqrel.Relators]
FE:92 [in coqrel.Relators]
FV1:100 [in coqrel.Relators]
FV1:158 [in coqrel.RelDefinitions]
FV1:194 [in coqrel.RelDefinitions]
FV1:41 [in coqrel.Relators]
FV1:53 [in coqrel.Relators]
FV1:61 [in coqrel.Relators]
FV1:72 [in coqrel.Relators]
FV2:101 [in coqrel.Relators]
FV2:159 [in coqrel.RelDefinitions]
FV2:195 [in coqrel.RelDefinitions]
FV2:42 [in coqrel.Relators]
FV2:54 [in coqrel.Relators]
FV2:62 [in coqrel.Relators]
FV2:73 [in coqrel.Relators]
F1:181 [in coqrel.RelDefinitions]
F1:88 [in coqrel.Relators]
F2:182 [in coqrel.RelDefinitions]
F2:89 [in coqrel.Relators]
f:103 [in coqrel.Relators]
f:103 [in coqrel.LogicalRelationsTests]
f:117 [in coqrel.LogicalRelationsTests]
f:121 [in coqrel.LogicalRelationsTests]
f:125 [in coqrel.RelDefinitions]
f:129 [in coqrel.LogicalRelationsTests]
f:139 [in coqrel.RelDefinitions]
f:147 [in coqrel.Monotonicity]
f:149 [in coqrel.RelDefinitions]
f:15 [in coqrel.Relators]
f:15 [in coqrel.MorphismsInterop]
f:155 [in coqrel.Monotonicity]
f:158 [in coqrel.Monotonicity]
f:165 [in coqrel.RelDefinitions]
f:18 [in coqrel.LogicalRelationsTests]
f:186 [in coqrel.RelDefinitions]
f:197 [in coqrel.RelDefinitions]
f:203 [in coqrel.RelOperators]
f:205 [in coqrel.KLR]
f:207 [in coqrel.LogicalRelationsTests]
f:212 [in coqrel.RelOperators]
f:216 [in coqrel.RelOperators]
f:218 [in coqrel.LogicalRelationsTests]
f:22 [in coqrel.Relators]
f:220 [in coqrel.RelOperators]
f:228 [in coqrel.RelOperators]
f:237 [in coqrel.LogicalRelationsTests]
f:238 [in coqrel.RelOperators]
f:243 [in coqrel.LogicalRelationsTests]
f:247 [in coqrel.RelOperators]
f:250 [in coqrel.KLR]
f:258 [in coqrel.RelOperators]
f:263 [in coqrel.KLR]
f:269 [in coqrel.RelOperators]
f:27 [in coqrel.MorphismsInterop]
f:272 [in coqrel.KLR]
f:273 [in coqrel.RelOperators]
f:296 [in coqrel.RelOperators]
f:302 [in coqrel.RelOperators]
f:331 [in coqrel.RelOperators]
f:34 [in coqrel.MorphismsInterop]
f:35 [in coqrel.Monotonicity]
f:35 [in coqrel.LogicalRelationsTests]
f:44 [in coqrel.Monotonicity]
f:44 [in coqrel.MorphismsInterop]
f:47 [in coqrel.Relators]
f:5 [in coqrel.Relators]
f:50 [in coqrel.Monotonicity]
f:50 [in coqrel.MorphismsInterop]
f:57 [in coqrel.Relators]
f:64 [in coqrel.Relators]
f:65 [in coqrel.LogicalRelationsTests]
f:69 [in coqrel.Monotonicity]
f:7 [in coqrel.MorphismsInterop]
f:79 [in coqrel.Relators]
f:80 [in coqrel.Monotonicity]
f:89 [in coqrel.RelDefinitions]
f:93 [in coqrel.Relators]
f:96 [in coqrel.LogicalRelationsTests]
G
g:104 [in coqrel.Relators]g:126 [in coqrel.RelDefinitions]
g:140 [in coqrel.RelDefinitions]
g:150 [in coqrel.RelDefinitions]
g:159 [in coqrel.Monotonicity]
g:16 [in coqrel.Relators]
g:16 [in coqrel.MorphismsInterop]
g:166 [in coqrel.RelDefinitions]
g:187 [in coqrel.RelDefinitions]
g:198 [in coqrel.RelDefinitions]
g:204 [in coqrel.RelOperators]
g:206 [in coqrel.KLR]
g:208 [in coqrel.LogicalRelationsTests]
g:213 [in coqrel.RelOperators]
g:219 [in coqrel.LogicalRelationsTests]
g:229 [in coqrel.RelOperators]
g:23 [in coqrel.Relators]
g:239 [in coqrel.RelOperators]
g:245 [in coqrel.LogicalRelationsTests]
g:248 [in coqrel.RelOperators]
g:259 [in coqrel.RelOperators]
g:270 [in coqrel.RelOperators]
g:28 [in coqrel.MorphismsInterop]
g:332 [in coqrel.RelOperators]
g:35 [in coqrel.MorphismsInterop]
g:36 [in coqrel.Monotonicity]
g:45 [in coqrel.Monotonicity]
g:45 [in coqrel.MorphismsInterop]
g:48 [in coqrel.Relators]
g:51 [in coqrel.Monotonicity]
g:51 [in coqrel.MorphismsInterop]
g:58 [in coqrel.Relators]
g:6 [in coqrel.Relators]
g:65 [in coqrel.Relators]
g:70 [in coqrel.Monotonicity]
g:8 [in coqrel.MorphismsInterop]
g:80 [in coqrel.Relators]
g:81 [in coqrel.Monotonicity]
g:90 [in coqrel.RelDefinitions]
g:94 [in coqrel.Relators]
H
HopA:175 [in coqrel.LogicalRelationsTests]HopB:176 [in coqrel.LogicalRelationsTests]
Hop:48 [in coqrel.LogicalRelationsTests]
HR:12 [in coqrel.LogicalRelationsTests]
HR:247 [in coqrel.Relators]
HR:25 [in coqrel.RelQuotient]
HR:26 [in coqrel.RelQuotient]
HR:268 [in coqrel.Relators]
HR:27 [in coqrel.RelQuotient]
HR:271 [in coqrel.Relators]
HR:274 [in coqrel.Relators]
HR:277 [in coqrel.Relators]
HT:10 [in coqrel.Delay]
Hux:14 [in coqrel.PreOrderTactic]
Hw':158 [in coqrel.KLR]
Hxa:177 [in coqrel.LogicalRelationsTests]
Hxb:178 [in coqrel.LogicalRelationsTests]
Hxy:51 [in coqrel.LogicalRelationsTests]
Hya:179 [in coqrel.LogicalRelationsTests]
Hyb:180 [in coqrel.LogicalRelationsTests]
h1:19 [in coqrel.Monotonicity]
H1:19 [in coqrel.BoolRel]
H1:7 [in coqrel.BoolRel]
H1:9 [in coqrel.BoolRel]
H2:10 [in coqrel.BoolRel]
H2:18 [in coqrel.BoolRel]
h2:20 [in coqrel.Monotonicity]
H2:8 [in coqrel.BoolRel]
h:10 [in coqrel.Monotonicity]
H:126 [in coqrel.Relators]
H:13 [in coqrel.LogicalRelationsTests]
H:144 [in coqrel.Relators]
H:16 [in coqrel.PreOrderTactic]
H:191 [in coqrel.RelOperators]
H:198 [in coqrel.RelOperators]
H:199 [in coqrel.LogicalRelationsTests]
h:230 [in coqrel.RelOperators]
H:25 [in coqrel.RelClasses]
H:31 [in coqrel.Relators]
H:32 [in coqrel.LogicalRelationsTests]
H:39 [in coqrel.Relators]
H:49 [in coqrel.RelDefinitions]
H:64 [in coqrel.Transport]
I
I:359 [in coqrel.RelOperators]I:365 [in coqrel.RelOperators]
K
kf:139 [in coqrel.KLR]kf:200 [in coqrel.KLR]
kf:223 [in coqrel.KLR]
kf:26 [in coqrel.KLR]
kf:90 [in coqrel.KLR]
L
L1:198 [in coqrel.KLR]l1:207 [in coqrel.KLR]
l1:215 [in coqrel.KLR]
l1:231 [in coqrel.LogicalRelationsTests]
L2:199 [in coqrel.KLR]
l2:208 [in coqrel.KLR]
l2:218 [in coqrel.KLR]
l2:232 [in coqrel.LogicalRelationsTests]
l:142 [in coqrel.KLR]
l:152 [in coqrel.KLR]
l:161 [in coqrel.KLR]
l:171 [in coqrel.KLR]
l:181 [in coqrel.KLR]
l:189 [in coqrel.KLR]
L:4 [in coqrel.KLR]
M
m1:12 [in coqrel.Monotonicity]m1:145 [in coqrel.Monotonicity]
m1:153 [in coqrel.Monotonicity]
m1:23 [in coqrel.Monotonicity]
m1:3 [in coqrel.Monotonicity]
m1:33 [in coqrel.Monotonicity]
m1:42 [in coqrel.Monotonicity]
m1:59 [in coqrel.Monotonicity]
m1:66 [in coqrel.Monotonicity]
m1:77 [in coqrel.Monotonicity]
m2:13 [in coqrel.Monotonicity]
m2:146 [in coqrel.Monotonicity]
m2:154 [in coqrel.Monotonicity]
m2:24 [in coqrel.Monotonicity]
m2:34 [in coqrel.Monotonicity]
m2:4 [in coqrel.Monotonicity]
m2:43 [in coqrel.Monotonicity]
m2:60 [in coqrel.Monotonicity]
m2:67 [in coqrel.Monotonicity]
m2:78 [in coqrel.Monotonicity]
m:100 [in coqrel.Monotonicity]
m:115 [in coqrel.Monotonicity]
m:12 [in coqrel.RDestruct]
m:124 [in coqrel.Monotonicity]
m:135 [in coqrel.Monotonicity]
m:151 [in coqrel.RelDefinitions]
m:160 [in coqrel.Monotonicity]
m:17 [in coqrel.MorphismsInterop]
m:209 [in coqrel.RelDefinitions]
m:21 [in coqrel.RDestruct]
m:214 [in coqrel.RelDefinitions]
m:230 [in coqrel.RelDefinitions]
m:236 [in coqrel.RelDefinitions]
m:24 [in coqrel.Relators]
m:28 [in coqrel.RDestruct]
m:379 [in coqrel.RelOperators]
m:39 [in coqrel.RelDefinitions]
m:405 [in coqrel.RelOperators]
m:436 [in coqrel.RelOperators]
m:5 [in coqrel.RDestruct]
m:54 [in coqrel.RelDefinitions]
m:56 [in coqrel.LogicalRelationsTests]
m:62 [in coqrel.RelDefinitions]
m:67 [in coqrel.RelDefinitions]
m:76 [in coqrel.RelDefinitions]
m:8 [in coqrel.PreOrderTactic]
m:83 [in coqrel.RelDefinitions]
m:94 [in coqrel.Monotonicity]
m:97 [in coqrel.RelDefinitions]
N
n:101 [in coqrel.Monotonicity]n:116 [in coqrel.Monotonicity]
n:125 [in coqrel.Monotonicity]
n:13 [in coqrel.RDestruct]
n:136 [in coqrel.Monotonicity]
n:14 [in coqrel.Monotonicity]
n:152 [in coqrel.RelDefinitions]
n:161 [in coqrel.Monotonicity]
n:18 [in coqrel.MorphismsInterop]
n:210 [in coqrel.RelDefinitions]
n:215 [in coqrel.RelDefinitions]
n:22 [in coqrel.RDestruct]
n:231 [in coqrel.RelDefinitions]
n:237 [in coqrel.RelDefinitions]
n:25 [in coqrel.Relators]
n:25 [in coqrel.Monotonicity]
n:29 [in coqrel.RDestruct]
n:32 [in coqrel.Monotonicity]
n:380 [in coqrel.RelOperators]
n:40 [in coqrel.RelDefinitions]
n:406 [in coqrel.RelOperators]
n:437 [in coqrel.RelOperators]
n:5 [in coqrel.Monotonicity]
n:55 [in coqrel.RelDefinitions]
n:57 [in coqrel.LogicalRelationsTests]
n:6 [in coqrel.RDestruct]
n:63 [in coqrel.RelDefinitions]
n:68 [in coqrel.RelDefinitions]
n:71 [in coqrel.Monotonicity]
n:77 [in coqrel.RelDefinitions]
n:84 [in coqrel.RelDefinitions]
n:95 [in coqrel.Monotonicity]
n:98 [in coqrel.RelDefinitions]
O
opA:171 [in coqrel.LogicalRelationsTests]opB:172 [in coqrel.LogicalRelationsTests]
op:47 [in coqrel.LogicalRelationsTests]
P
pat:216 [in coqrel.KLR]pat:219 [in coqrel.KLR]
PA:6 [in coqrel.Transport]
PB:7 [in coqrel.Transport]
P1:1 [in coqrel.BoolRel]
P1:11 [in coqrel.BoolRel]
p1:21 [in coqrel.Monotonicity]
P2:12 [in coqrel.BoolRel]
P2:2 [in coqrel.BoolRel]
p2:22 [in coqrel.Monotonicity]
P:1 [in coqrel.Delay]
P:1 [in coqrel.LogicalRelationsTests]
P:107 [in coqrel.Relators]
P:108 [in coqrel.Monotonicity]
P:11 [in coqrel.Delay]
p:11 [in coqrel.Monotonicity]
P:117 [in coqrel.RelDefinitions]
P:117 [in coqrel.Monotonicity]
P:122 [in coqrel.Monotonicity]
P:126 [in coqrel.Monotonicity]
P:132 [in coqrel.RelOperators]
P:137 [in coqrel.Monotonicity]
P:15 [in coqrel.RDestruct]
P:15 [in coqrel.RelDefinitions]
P:153 [in coqrel.RelDefinitions]
P:162 [in coqrel.Monotonicity]
P:167 [in coqrel.KLR]
p:19 [in coqrel.LogicalRelationsTests]
P:19 [in coqrel.MorphismsInterop]
P:194 [in coqrel.KLR]
P:20 [in coqrel.RelDefinitions]
P:202 [in coqrel.RelDefinitions]
P:209 [in coqrel.Relators]
P:21 [in coqrel.BoolRel]
P:216 [in coqrel.RelDefinitions]
P:22 [in coqrel.MorphismsInterop]
P:222 [in coqrel.RelDefinitions]
P:244 [in coqrel.KLR]
P:252 [in coqrel.RelOperators]
P:26 [in coqrel.Relators]
P:27 [in coqrel.RelDefinitions]
P:277 [in coqrel.KLR]
P:30 [in coqrel.RelDefinitions]
P:333 [in coqrel.RelOperators]
P:346 [in coqrel.RelOperators]
P:353 [in coqrel.RelOperators]
P:37 [in coqrel.RelDefinitions]
P:37 [in coqrel.MorphismsInterop]
P:388 [in coqrel.RelOperators]
P:4 [in coqrel.Delay]
P:413 [in coqrel.RelOperators]
P:44 [in coqrel.KLR]
P:447 [in coqrel.RelOperators]
P:5 [in coqrel.Delay]
P:52 [in coqrel.RelDefinitions]
P:53 [in coqrel.MorphismsInterop]
P:55 [in coqrel.Transport]
P:6 [in coqrel.Delay]
P:60 [in coqrel.RelDefinitions]
P:61 [in coqrel.KLR]
P:67 [in coqrel.Relators]
P:69 [in coqrel.RelDefinitions]
P:7 [in coqrel.Delay]
P:82 [in coqrel.KLR]
P:85 [in coqrel.RelDefinitions]
P:87 [in coqrel.Monotonicity]
Q
Q':119 [in coqrel.Monotonicity]Q':335 [in coqrel.RelOperators]
Q1:13 [in coqrel.BoolRel]
Q1:3 [in coqrel.BoolRel]
Q2:14 [in coqrel.BoolRel]
Q2:4 [in coqrel.BoolRel]
Q:108 [in coqrel.Relators]
Q:109 [in coqrel.Monotonicity]
Q:118 [in coqrel.RelDefinitions]
Q:118 [in coqrel.Monotonicity]
Q:12 [in coqrel.Delay]
Q:127 [in coqrel.Monotonicity]
Q:154 [in coqrel.RelDefinitions]
Q:16 [in coqrel.RDestruct]
Q:163 [in coqrel.Monotonicity]
Q:168 [in coqrel.KLR]
Q:195 [in coqrel.KLR]
Q:2 [in coqrel.LogicalRelationsTests]
Q:20 [in coqrel.MorphismsInterop]
Q:203 [in coqrel.RelDefinitions]
Q:21 [in coqrel.RelDefinitions]
Q:217 [in coqrel.RelDefinitions]
Q:23 [in coqrel.RDestruct]
Q:24 [in coqrel.RelDefinitions]
Q:245 [in coqrel.KLR]
Q:253 [in coqrel.RelOperators]
Q:27 [in coqrel.Relators]
Q:278 [in coqrel.KLR]
Q:30 [in coqrel.RDestruct]
Q:31 [in coqrel.RelDefinitions]
Q:334 [in coqrel.RelOperators]
Q:38 [in coqrel.MorphismsInterop]
Q:389 [in coqrel.RelOperators]
Q:414 [in coqrel.RelOperators]
Q:45 [in coqrel.KLR]
Q:52 [in coqrel.Monotonicity]
Q:54 [in coqrel.MorphismsInterop]
Q:56 [in coqrel.Transport]
Q:62 [in coqrel.KLR]
Q:67 [in coqrel.Transport]
Q:68 [in coqrel.Relators]
Q:7 [in coqrel.RDestruct]
Q:70 [in coqrel.RelDefinitions]
Q:83 [in coqrel.KLR]
Q:88 [in coqrel.Monotonicity]
R
RAB:13 [in coqrel.RelClasses]RAB:151 [in coqrel.RelOperators]
RAB:172 [in coqrel.RelOperators]
RAB:178 [in coqrel.RelOperators]
RAB:183 [in coqrel.RelOperators]
RAB:29 [in coqrel.RelClasses]
RAC:15 [in coqrel.RelClasses]
RAC:31 [in coqrel.RelClasses]
RAuto0:65 [in coqrel.Transport]
RA12:48 [in coqrel.RelClasses]
RA13:50 [in coqrel.RelClasses]
RA23:49 [in coqrel.RelClasses]
RA:123 [in coqrel.RelDefinitions]
RA:13 [in coqrel.MorphismsInterop]
RA:137 [in coqrel.RelDefinitions]
RA:14 [in coqrel.KLR]
RA:147 [in coqrel.RelDefinitions]
RA:153 [in coqrel.Relators]
RA:157 [in coqrel.Relators]
RA:159 [in coqrel.Relators]
RA:173 [in coqrel.LogicalRelationsTests]
RA:189 [in coqrel.Relators]
RA:193 [in coqrel.Relators]
RA:195 [in coqrel.Relators]
RA:197 [in coqrel.Relators]
RA:207 [in coqrel.Relators]
RA:22 [in coqrel.LogicalRelationsTests]
RA:236 [in coqrel.Relators]
RA:24 [in coqrel.OptionRel]
RA:248 [in coqrel.Relators]
RA:28 [in coqrel.OptionRel]
RA:280 [in coqrel.Relators]
RA:282 [in coqrel.Relators]
RA:284 [in coqrel.Relators]
RA:3 [in coqrel.OptionRel]
RA:39 [in coqrel.RelClasses]
RA:43 [in coqrel.RelClasses]
RA:49 [in coqrel.OptionRel]
RA:5 [in coqrel.MorphismsInterop]
RA:54 [in coqrel.LogicalRelationsTests]
RA:61 [in coqrel.LogicalRelationsTests]
RA:68 [in coqrel.LogicalRelationsTests]
RBC:14 [in coqrel.RelClasses]
RBC:152 [in coqrel.RelOperators]
RBC:173 [in coqrel.RelOperators]
RBC:179 [in coqrel.RelOperators]
RBC:184 [in coqrel.RelOperators]
RBC:30 [in coqrel.RelClasses]
RB12:54 [in coqrel.RelClasses]
RB13:56 [in coqrel.RelClasses]
RB23:55 [in coqrel.RelClasses]
RB:124 [in coqrel.RelDefinitions]
RB:138 [in coqrel.RelDefinitions]
RB:14 [in coqrel.MorphismsInterop]
RB:148 [in coqrel.RelDefinitions]
RB:15 [in coqrel.KLR]
RB:154 [in coqrel.Relators]
RB:158 [in coqrel.Relators]
RB:160 [in coqrel.Relators]
RB:174 [in coqrel.LogicalRelationsTests]
RB:190 [in coqrel.Relators]
RB:194 [in coqrel.Relators]
RB:196 [in coqrel.Relators]
RB:198 [in coqrel.Relators]
RB:208 [in coqrel.Relators]
RB:249 [in coqrel.Relators]
RB:25 [in coqrel.OptionRel]
RB:25 [in coqrel.LogicalRelationsTests]
RB:281 [in coqrel.Relators]
RB:283 [in coqrel.Relators]
RB:285 [in coqrel.Relators]
RB:4 [in coqrel.Relators]
RB:40 [in coqrel.RelClasses]
RB:44 [in coqrel.RelClasses]
RB:50 [in coqrel.OptionRel]
RB:55 [in coqrel.LogicalRelationsTests]
RB:6 [in coqrel.MorphismsInterop]
RB:62 [in coqrel.LogicalRelationsTests]
RB:69 [in coqrel.LogicalRelationsTests]
RCD:174 [in coqrel.RelOperators]
Rc:138 [in coqrel.Monotonicity]
Rc:235 [in coqrel.RelDefinitions]
Rg:139 [in coqrel.Monotonicity]
RR:46 [in coqrel.KLR]
RR:51 [in coqrel.KLR]
RR:56 [in coqrel.KLR]
RR:63 [in coqrel.KLR]
RR:70 [in coqrel.KLR]
RR:76 [in coqrel.KLR]
RR:84 [in coqrel.KLR]
RW1:257 [in coqrel.KLR]
RW2:258 [in coqrel.KLR]
R':105 [in coqrel.Monotonicity]
R':120 [in coqrel.LogicalRelationsTests]
R':230 [in coqrel.LogicalRelationsTests]
R':49 [in coqrel.Monotonicity]
R':58 [in coqrel.Monotonicity]
R':68 [in coqrel.Monotonicity]
R':79 [in coqrel.Monotonicity]
R':94 [in coqrel.LogicalRelationsTests]
R':96 [in coqrel.RelOperators]
R':99 [in coqrel.Monotonicity]
R1':157 [in coqrel.LogicalRelationsTests]
R1':189 [in coqrel.LogicalRelationsTests]
R1':41 [in coqrel.LogicalRelationsTests]
R12:231 [in coqrel.RelOperators]
R13:233 [in coqrel.RelOperators]
R1:101 [in coqrel.RelDefinitions]
R1:107 [in coqrel.RelOperators]
R1:11 [in coqrel.RelOperators]
R1:111 [in coqrel.RelDefinitions]
R1:113 [in coqrel.RelOperators]
R1:119 [in coqrel.RelOperators]
R1:123 [in coqrel.LogicalRelationsTests]
R1:138 [in coqrel.LogicalRelationsTests]
R1:14 [in coqrel.Transport]
R1:155 [in coqrel.LogicalRelationsTests]
R1:167 [in coqrel.Relators]
R1:17 [in coqrel.RelOperators]
R1:171 [in coqrel.Relators]
R1:175 [in coqrel.Relators]
R1:179 [in coqrel.Relators]
R1:183 [in coqrel.Relators]
R1:187 [in coqrel.LogicalRelationsTests]
R1:215 [in coqrel.LogicalRelationsTests]
R1:216 [in coqrel.Relators]
R1:220 [in coqrel.Relators]
R1:224 [in coqrel.Relators]
R1:228 [in coqrel.Relators]
R1:232 [in coqrel.Relators]
R1:24 [in coqrel.RelOperators]
R1:29 [in coqrel.RelOperators]
R1:3 [in coqrel.RelOperators]
R1:33 [in coqrel.RelOperators]
R1:37 [in coqrel.RelOperators]
R1:40 [in coqrel.RelOperators]
R1:40 [in coqrel.LogicalRelationsTests]
R1:43 [in coqrel.RelOperators]
R1:46 [in coqrel.RelOperators]
R1:47 [in coqrel.KLR]
R1:50 [in coqrel.RelOperators]
R1:52 [in coqrel.KLR]
R1:57 [in coqrel.KLR]
R1:58 [in coqrel.RelOperators]
R1:61 [in coqrel.MorphismsInterop]
R1:64 [in coqrel.KLR]
R1:64 [in coqrel.RelOperators]
R1:69 [in coqrel.RelOperators]
R1:71 [in coqrel.KLR]
R1:75 [in coqrel.RelOperators]
R1:77 [in coqrel.KLR]
R1:78 [in coqrel.RelOperators]
R1:81 [in coqrel.RelOperators]
R1:84 [in coqrel.RelOperators]
R1:85 [in coqrel.KLR]
R1:87 [in coqrel.RelOperators]
R1:90 [in coqrel.RelOperators]
R1:99 [in coqrel.RelOperators]
R2':43 [in coqrel.LogicalRelationsTests]
R23:232 [in coqrel.RelOperators]
R2:100 [in coqrel.RelOperators]
R2:102 [in coqrel.RelDefinitions]
R2:108 [in coqrel.RelOperators]
R2:112 [in coqrel.RelDefinitions]
R2:114 [in coqrel.RelOperators]
R2:12 [in coqrel.RelOperators]
R2:120 [in coqrel.RelOperators]
R2:124 [in coqrel.LogicalRelationsTests]
R2:139 [in coqrel.LogicalRelationsTests]
R2:15 [in coqrel.Transport]
R2:156 [in coqrel.LogicalRelationsTests]
R2:168 [in coqrel.Relators]
R2:172 [in coqrel.Relators]
R2:176 [in coqrel.Relators]
R2:18 [in coqrel.RelOperators]
R2:180 [in coqrel.Relators]
R2:184 [in coqrel.Relators]
R2:188 [in coqrel.LogicalRelationsTests]
R2:216 [in coqrel.LogicalRelationsTests]
R2:217 [in coqrel.Relators]
R2:221 [in coqrel.Relators]
R2:225 [in coqrel.Relators]
R2:229 [in coqrel.Relators]
R2:233 [in coqrel.Relators]
R2:25 [in coqrel.RelOperators]
R2:30 [in coqrel.RelOperators]
R2:34 [in coqrel.RelOperators]
R2:38 [in coqrel.RelOperators]
R2:4 [in coqrel.RelOperators]
R2:41 [in coqrel.RelOperators]
R2:42 [in coqrel.LogicalRelationsTests]
R2:44 [in coqrel.RelOperators]
R2:47 [in coqrel.RelOperators]
R2:51 [in coqrel.RelOperators]
R2:59 [in coqrel.RelOperators]
R2:62 [in coqrel.MorphismsInterop]
R2:65 [in coqrel.KLR]
R2:65 [in coqrel.RelOperators]
R2:70 [in coqrel.RelOperators]
R2:72 [in coqrel.KLR]
R2:76 [in coqrel.RelOperators]
R2:78 [in coqrel.KLR]
R2:79 [in coqrel.RelOperators]
R2:82 [in coqrel.RelOperators]
R2:85 [in coqrel.RelOperators]
R2:86 [in coqrel.KLR]
R2:88 [in coqrel.RelOperators]
R2:91 [in coqrel.RelOperators]
R3:217 [in coqrel.LogicalRelationsTests]
R:102 [in coqrel.Relators]
R:102 [in coqrel.LogicalRelationsTests]
R:104 [in coqrel.Monotonicity]
R:108 [in coqrel.RelDefinitions]
R:108 [in coqrel.LogicalRelationsTests]
R:11 [in coqrel.OptionRel]
R:110 [in coqrel.KLR]
R:111 [in coqrel.Relators]
R:112 [in coqrel.LogicalRelationsTests]
R:114 [in coqrel.Monotonicity]
R:116 [in coqrel.LogicalRelationsTests]
R:118 [in coqrel.KLR]
R:119 [in coqrel.Relators]
R:119 [in coqrel.LogicalRelationsTests]
R:123 [in coqrel.Monotonicity]
R:127 [in coqrel.RelOperators]
R:128 [in coqrel.LogicalRelationsTests]
R:129 [in coqrel.Relators]
R:13 [in coqrel.RelQuotient]
R:134 [in coqrel.Monotonicity]
R:137 [in coqrel.Relators]
R:14 [in coqrel.OptionRel]
R:14 [in coqrel.Relators]
R:14 [in coqrel.RDestruct]
R:140 [in coqrel.LogicalRelationsTests]
R:143 [in coqrel.KLR]
R:152 [in coqrel.Monotonicity]
R:153 [in coqrel.KLR]
R:158 [in coqrel.LogicalRelationsTests]
R:162 [in coqrel.KLR]
R:164 [in coqrel.RelOperators]
R:167 [in coqrel.RelOperators]
R:17 [in coqrel.LogicalRelationsTests]
R:172 [in coqrel.KLR]
R:18 [in coqrel.RelQuotient]
R:182 [in coqrel.KLR]
R:190 [in coqrel.KLR]
R:190 [in coqrel.LogicalRelationsTests]
R:194 [in coqrel.LogicalRelationsTests]
R:196 [in coqrel.RelDefinitions]
R:2 [in coqrel.RelClasses]
R:2 [in coqrel.RelQuotient]
R:20 [in coqrel.RelQuotient]
R:203 [in coqrel.KLR]
R:205 [in coqrel.RelOperators]
R:206 [in coqrel.LogicalRelationsTests]
R:208 [in coqrel.RelDefinitions]
R:21 [in coqrel.OptionRel]
R:21 [in coqrel.Relators]
R:212 [in coqrel.KLR]
R:213 [in coqrel.RelDefinitions]
R:217 [in coqrel.RelOperators]
R:22 [in coqrel.RelClasses]
R:22 [in coqrel.RelQuotient]
R:220 [in coqrel.RelDefinitions]
R:221 [in coqrel.RelOperators]
R:225 [in coqrel.RelDefinitions]
R:226 [in coqrel.KLR]
R:229 [in coqrel.RelDefinitions]
R:229 [in coqrel.LogicalRelationsTests]
R:23 [in coqrel.OptionRel]
R:23 [in coqrel.RelOperators]
R:234 [in coqrel.KLR]
R:234 [in coqrel.RelDefinitions]
R:238 [in coqrel.LogicalRelationsTests]
R:24 [in coqrel.Transport]
R:240 [in coqrel.KLR]
R:240 [in coqrel.RelOperators]
R:241 [in coqrel.Relators]
R:242 [in coqrel.Relators]
R:244 [in coqrel.LogicalRelationsTests]
R:249 [in coqrel.RelOperators]
R:251 [in coqrel.KLR]
R:252 [in coqrel.Relators]
R:259 [in coqrel.Relators]
R:26 [in coqrel.MorphismsInterop]
R:260 [in coqrel.RelOperators]
R:262 [in coqrel.Relators]
R:263 [in coqrel.Relators]
R:264 [in coqrel.KLR]
R:273 [in coqrel.KLR]
R:274 [in coqrel.RelOperators]
R:278 [in coqrel.Relators]
R:279 [in coqrel.Relators]
R:28 [in coqrel.RelOperators]
R:283 [in coqrel.RelOperators]
R:292 [in coqrel.RelOperators]
R:3 [in coqrel.Transport]
R:3 [in coqrel.PreOrderTactic]
R:31 [in coqrel.LogicalRelationsTests]
R:311 [in coqrel.RelOperators]
R:318 [in coqrel.RelOperators]
R:33 [in coqrel.Transport]
R:33 [in coqrel.KLR]
R:33 [in coqrel.RelDefinitions]
R:33 [in coqrel.MorphismsInterop]
R:330 [in coqrel.RelOperators]
R:35 [in coqrel.RelOperators]
R:36 [in coqrel.OptionRel]
R:36 [in coqrel.KLR]
R:369 [in coqrel.RelOperators]
R:378 [in coqrel.RelOperators]
R:38 [in coqrel.RelDefinitions]
R:385 [in coqrel.RelOperators]
R:39 [in coqrel.OptionRel]
R:394 [in coqrel.RelOperators]
R:40 [in coqrel.KLR]
R:403 [in coqrel.RelOperators]
R:410 [in coqrel.RelOperators]
R:420 [in coqrel.RelOperators]
R:43 [in coqrel.MorphismsInterop]
R:433 [in coqrel.RelOperators]
R:442 [in coqrel.RelOperators]
R:46 [in coqrel.Transport]
R:46 [in coqrel.OptionRel]
R:46 [in coqrel.LogicalRelationsTests]
R:48 [in coqrel.OptionRel]
R:49 [in coqrel.MorphismsInterop]
R:53 [in coqrel.OptionRel]
R:53 [in coqrel.RelDefinitions]
R:57 [in coqrel.Monotonicity]
R:58 [in coqrel.MorphismsInterop]
R:60 [in coqrel.OptionRel]
R:61 [in coqrel.RelDefinitions]
R:63 [in coqrel.Relators]
R:65 [in coqrel.Monotonicity]
R:66 [in coqrel.RelDefinitions]
R:66 [in coqrel.RelOperators]
R:7 [in coqrel.PreOrderTactic]
R:71 [in coqrel.RelOperators]
R:74 [in coqrel.RelOperators]
R:75 [in coqrel.RelDefinitions]
R:76 [in coqrel.Monotonicity]
R:78 [in coqrel.LogicalRelationsTests]
R:80 [in coqrel.RelDefinitions]
R:84 [in coqrel.Monotonicity]
R:86 [in coqrel.LogicalRelationsTests]
R:9 [in coqrel.RelClasses]
R:9 [in coqrel.RelQuotient]
R:91 [in coqrel.RelDefinitions]
R:93 [in coqrel.RelOperators]
R:93 [in coqrel.Monotonicity]
R:93 [in coqrel.LogicalRelationsTests]
R:95 [in coqrel.RelOperators]
R:96 [in coqrel.RelDefinitions]
R:98 [in coqrel.Monotonicity]
S
sA:112 [in coqrel.Relators]sA:112 [in coqrel.KLR]
sA:120 [in coqrel.KLR]
sA:130 [in coqrel.Relators]
sA:25 [in coqrel.Transport]
sA:34 [in coqrel.Transport]
sA:47 [in coqrel.Transport]
sB:113 [in coqrel.Relators]
sB:113 [in coqrel.KLR]
sB:121 [in coqrel.KLR]
sB:131 [in coqrel.Relators]
sB:26 [in coqrel.Transport]
sB:35 [in coqrel.Transport]
sB:48 [in coqrel.Transport]
S:195 [in coqrel.LogicalRelationsTests]
S:95 [in coqrel.LogicalRelationsTests]
T
Tw:446 [in coqrel.RelOperators]T:196 [in coqrel.LogicalRelationsTests]
t:203 [in coqrel.LogicalRelationsTests]
T:221 [in coqrel.RelDefinitions]
t:27 [in coqrel.LogicalRelationsTests]
T:28 [in coqrel.Relators]
T:32 [in coqrel.Relators]
T:444 [in coqrel.RelOperators]
T:81 [in coqrel.RelDefinitions]
U
Unconvertible0:66 [in coqrel.Transport]u:11 [in coqrel.RelQuotient]
u:16 [in coqrel.RelQuotient]
u:188 [in coqrel.RelDefinitions]
V
var1:49 [in coqrel.KLR]var1:67 [in coqrel.KLR]
var2:68 [in coqrel.KLR]
var:35 [in coqrel.KLR]
var:50 [in coqrel.KLR]
var:69 [in coqrel.KLR]
v1:105 [in coqrel.Relators]
V1:155 [in coqrel.RelDefinitions]
v1:160 [in coqrel.RelDefinitions]
v1:162 [in coqrel.RelDefinitions]
v1:167 [in coqrel.RelDefinitions]
v1:170 [in coqrel.RelDefinitions]
v1:173 [in coqrel.RelDefinitions]
V1:178 [in coqrel.RelDefinitions]
V1:191 [in coqrel.RelDefinitions]
v1:199 [in coqrel.RelDefinitions]
V1:69 [in coqrel.Relators]
v1:74 [in coqrel.Relators]
v1:76 [in coqrel.Relators]
v1:81 [in coqrel.Relators]
v1:83 [in coqrel.Relators]
V1:85 [in coqrel.Relators]
v1:90 [in coqrel.Relators]
v1:95 [in coqrel.Relators]
V1:97 [in coqrel.Relators]
v2:106 [in coqrel.Relators]
V2:156 [in coqrel.RelDefinitions]
v2:161 [in coqrel.RelDefinitions]
v2:163 [in coqrel.RelDefinitions]
v2:168 [in coqrel.RelDefinitions]
v2:171 [in coqrel.RelDefinitions]
v2:174 [in coqrel.RelDefinitions]
V2:179 [in coqrel.RelDefinitions]
V2:192 [in coqrel.RelDefinitions]
v2:200 [in coqrel.RelDefinitions]
V2:70 [in coqrel.Relators]
v2:75 [in coqrel.Relators]
v2:77 [in coqrel.Relators]
v2:82 [in coqrel.Relators]
v2:84 [in coqrel.Relators]
V2:86 [in coqrel.Relators]
v2:91 [in coqrel.Relators]
v2:96 [in coqrel.Relators]
V2:98 [in coqrel.Relators]
v:189 [in coqrel.RelDefinitions]
V:40 [in coqrel.Relators]
v:43 [in coqrel.Relators]
v:44 [in coqrel.Relators]
v:45 [in coqrel.Relators]
v:49 [in coqrel.Relators]
v:50 [in coqrel.Relators]
v:51 [in coqrel.Relators]
V:52 [in coqrel.Relators]
v:55 [in coqrel.Relators]
v:59 [in coqrel.Relators]
V:60 [in coqrel.Relators]
v:66 [in coqrel.Relators]
W
WA:8 [in coqrel.KLR]WB:11 [in coqrel.KLR]
w':147 [in coqrel.KLR]
w':157 [in coqrel.KLR]
w':164 [in coqrel.KLR]
w':176 [in coqrel.KLR]
w':184 [in coqrel.KLR]
w':196 [in coqrel.KLR]
w':209 [in coqrel.KLR]
w':220 [in coqrel.KLR]
w':424 [in coqrel.RelOperators]
w':435 [in coqrel.RelOperators]
w':448 [in coqrel.RelOperators]
W1:246 [in coqrel.KLR]
W1:253 [in coqrel.KLR]
W1:259 [in coqrel.KLR]
W1:268 [in coqrel.KLR]
W2:247 [in coqrel.KLR]
W2:254 [in coqrel.KLR]
W2:260 [in coqrel.KLR]
W2:269 [in coqrel.KLR]
W:1 [in coqrel.KLR]
w:111 [in coqrel.KLR]
w:119 [in coqrel.KLR]
W:124 [in coqrel.KLR]
W:127 [in coqrel.KLR]
W:130 [in coqrel.KLR]
w:144 [in coqrel.KLR]
w:154 [in coqrel.KLR]
w:163 [in coqrel.KLR]
w:173 [in coqrel.KLR]
w:18 [in coqrel.KLR]
w:183 [in coqrel.KLR]
w:191 [in coqrel.KLR]
W:197 [in coqrel.KLR]
w:204 [in coqrel.KLR]
w:21 [in coqrel.KLR]
W:210 [in coqrel.LogicalRelationsTests]
w:213 [in coqrel.KLR]
w:223 [in coqrel.LogicalRelationsTests]
w:224 [in coqrel.LogicalRelationsTests]
w:225 [in coqrel.LogicalRelationsTests]
w:229 [in coqrel.KLR]
w:237 [in coqrel.KLR]
w:241 [in coqrel.KLR]
w:252 [in coqrel.KLR]
w:265 [in coqrel.KLR]
w:274 [in coqrel.KLR]
w:34 [in coqrel.KLR]
w:37 [in coqrel.KLR]
w:41 [in coqrel.KLR]
W:416 [in coqrel.RelOperators]
w:421 [in coqrel.RelOperators]
W:425 [in coqrel.RelOperators]
W:429 [in coqrel.RelOperators]
w:434 [in coqrel.RelOperators]
W:438 [in coqrel.RelOperators]
w:443 [in coqrel.RelOperators]
w:445 [in coqrel.RelOperators]
w:48 [in coqrel.KLR]
W:5 [in coqrel.KLR]
w:53 [in coqrel.KLR]
w:58 [in coqrel.KLR]
w:66 [in coqrel.KLR]
w:73 [in coqrel.KLR]
w:79 [in coqrel.KLR]
w:87 [in coqrel.KLR]
X
xa1:163 [in coqrel.LogicalRelationsTests]xa2:164 [in coqrel.LogicalRelationsTests]
xb1:167 [in coqrel.LogicalRelationsTests]
xb2:168 [in coqrel.LogicalRelationsTests]
x1:113 [in coqrel.RelDefinitions]
x1:145 [in coqrel.LogicalRelationsTests]
x1:191 [in coqrel.Relators]
x1:279 [in coqrel.RelOperators]
x1:288 [in coqrel.RelOperators]
x1:97 [in coqrel.LogicalRelationsTests]
x2:114 [in coqrel.RelDefinitions]
x2:146 [in coqrel.LogicalRelationsTests]
x2:192 [in coqrel.Relators]
x2:280 [in coqrel.RelOperators]
x2:289 [in coqrel.RelOperators]
x2:99 [in coqrel.LogicalRelationsTests]
x:1 [in coqrel.RDestruct]
x:101 [in coqrel.RelOperators]
x:103 [in coqrel.RelDefinitions]
x:105 [in coqrel.LogicalRelationsTests]
x:106 [in coqrel.Monotonicity]
x:109 [in coqrel.RelOperators]
x:109 [in coqrel.LogicalRelationsTests]
x:11 [in coqrel.PreOrderTactic]
x:11 [in coqrel.RelDefinitions]
x:113 [in coqrel.LogicalRelationsTests]
x:115 [in coqrel.RelOperators]
x:123 [in coqrel.RelOperators]
x:127 [in coqrel.RelDefinitions]
x:13 [in coqrel.PreOrderTactic]
x:13 [in coqrel.RelOperators]
x:130 [in coqrel.RelOperators]
x:135 [in coqrel.RelOperators]
x:139 [in coqrel.RelOperators]
x:14 [in coqrel.RelQuotient]
x:140 [in coqrel.Monotonicity]
x:141 [in coqrel.RelDefinitions]
x:141 [in coqrel.LogicalRelationsTests]
x:145 [in coqrel.KLR]
x:15 [in coqrel.PreOrderTactic]
x:153 [in coqrel.RelOperators]
x:155 [in coqrel.KLR]
x:159 [in coqrel.LogicalRelationsTests]
x:16 [in coqrel.Transport]
x:165 [in coqrel.KLR]
x:17 [in coqrel.Relators]
x:17 [in coqrel.RelClasses]
x:174 [in coqrel.KLR]
x:183 [in coqrel.RelDefinitions]
x:185 [in coqrel.KLR]
x:19 [in coqrel.RelOperators]
x:191 [in coqrel.LogicalRelationsTests]
x:192 [in coqrel.KLR]
x:2 [in coqrel.RelDefinitions]
x:200 [in coqrel.LogicalRelationsTests]
x:206 [in coqrel.RelOperators]
X:209 [in coqrel.LogicalRelationsTests]
x:22 [in coqrel.BoolRel]
x:222 [in coqrel.LogicalRelationsTests]
x:227 [in coqrel.KLR]
x:23 [in coqrel.RelQuotient]
x:23 [in coqrel.LogicalRelationsTests]
x:233 [in coqrel.LogicalRelationsTests]
x:235 [in coqrel.KLR]
x:239 [in coqrel.LogicalRelationsTests]
x:24 [in coqrel.RDestruct]
x:241 [in coqrel.RelOperators]
x:242 [in coqrel.KLR]
x:246 [in coqrel.LogicalRelationsTests]
x:249 [in coqrel.LogicalRelationsTests]
x:250 [in coqrel.RelOperators]
x:253 [in coqrel.Relators]
x:253 [in coqrel.LogicalRelationsTests]
x:256 [in coqrel.LogicalRelationsTests]
x:258 [in coqrel.LogicalRelationsTests]
x:26 [in coqrel.Monotonicity]
x:263 [in coqrel.RelOperators]
x:266 [in coqrel.KLR]
x:27 [in coqrel.Monotonicity]
x:275 [in coqrel.KLR]
x:28 [in coqrel.RelQuotient]
x:31 [in coqrel.OptionRel]
x:31 [in coqrel.RDestruct]
x:33 [in coqrel.OptionRel]
x:33 [in coqrel.RelClasses]
x:33 [in coqrel.LogicalRelationsTests]
x:34 [in coqrel.RelDefinitions]
x:347 [in coqrel.RelOperators]
x:354 [in coqrel.RelOperators]
x:360 [in coqrel.RelOperators]
x:370 [in coqrel.RelOperators]
x:373 [in coqrel.RelOperators]
x:38 [in coqrel.KLR]
x:386 [in coqrel.RelOperators]
x:395 [in coqrel.RelOperators]
x:398 [in coqrel.RelOperators]
x:4 [in coqrel.RelClasses]
x:40 [in coqrel.OptionRel]
x:411 [in coqrel.RelOperators]
x:42 [in coqrel.KLR]
x:49 [in coqrel.LogicalRelationsTests]
x:5 [in coqrel.RelOperators]
x:52 [in coqrel.RelOperators]
x:54 [in coqrel.OptionRel]
x:54 [in coqrel.KLR]
x:58 [in coqrel.LogicalRelationsTests]
x:59 [in coqrel.KLR]
x:6 [in coqrel.OptionRel]
x:6 [in coqrel.RelQuotient]
x:60 [in coqrel.RelOperators]
x:61 [in coqrel.OptionRel]
x:63 [in coqrel.LogicalRelationsTests]
x:70 [in coqrel.LogicalRelationsTests]
x:74 [in coqrel.KLR]
x:8 [in coqrel.RDestruct]
x:80 [in coqrel.KLR]
x:80 [in coqrel.LogicalRelationsTests]
x:83 [in coqrel.LogicalRelationsTests]
x:85 [in coqrel.Monotonicity]
x:88 [in coqrel.LogicalRelationsTests]
x:9 [in coqrel.MorphismsInterop]
Y
ya1:165 [in coqrel.LogicalRelationsTests]ya2:166 [in coqrel.LogicalRelationsTests]
yb1:169 [in coqrel.LogicalRelationsTests]
yb2:170 [in coqrel.LogicalRelationsTests]
y1:115 [in coqrel.RelDefinitions]
y1:147 [in coqrel.LogicalRelationsTests]
y1:281 [in coqrel.RelOperators]
y1:290 [in coqrel.RelOperators]
y1:98 [in coqrel.LogicalRelationsTests]
y2:100 [in coqrel.LogicalRelationsTests]
y2:116 [in coqrel.RelDefinitions]
y2:148 [in coqrel.LogicalRelationsTests]
y2:282 [in coqrel.RelOperators]
y2:291 [in coqrel.RelOperators]
y:10 [in coqrel.MorphismsInterop]
y:102 [in coqrel.RelOperators]
y:104 [in coqrel.RelDefinitions]
y:106 [in coqrel.LogicalRelationsTests]
y:107 [in coqrel.Monotonicity]
y:110 [in coqrel.RelOperators]
y:110 [in coqrel.LogicalRelationsTests]
y:114 [in coqrel.LogicalRelationsTests]
y:116 [in coqrel.RelOperators]
y:12 [in coqrel.PreOrderTactic]
y:12 [in coqrel.RelDefinitions]
y:124 [in coqrel.RelOperators]
y:128 [in coqrel.RelDefinitions]
y:131 [in coqrel.RelOperators]
y:136 [in coqrel.RelOperators]
y:14 [in coqrel.RelOperators]
y:140 [in coqrel.RelOperators]
y:141 [in coqrel.Monotonicity]
y:142 [in coqrel.RelDefinitions]
y:142 [in coqrel.LogicalRelationsTests]
y:146 [in coqrel.KLR]
y:15 [in coqrel.OptionRel]
y:15 [in coqrel.RelQuotient]
y:155 [in coqrel.RelOperators]
y:156 [in coqrel.KLR]
y:160 [in coqrel.LogicalRelationsTests]
y:166 [in coqrel.KLR]
y:17 [in coqrel.Transport]
y:175 [in coqrel.KLR]
y:18 [in coqrel.RelClasses]
y:184 [in coqrel.RelDefinitions]
y:186 [in coqrel.KLR]
y:192 [in coqrel.LogicalRelationsTests]
y:193 [in coqrel.KLR]
y:2 [in coqrel.RDestruct]
y:20 [in coqrel.RelOperators]
y:201 [in coqrel.LogicalRelationsTests]
y:207 [in coqrel.RelOperators]
y:226 [in coqrel.LogicalRelationsTests]
y:228 [in coqrel.KLR]
y:23 [in coqrel.BoolRel]
y:234 [in coqrel.LogicalRelationsTests]
y:236 [in coqrel.KLR]
y:24 [in coqrel.LogicalRelationsTests]
y:240 [in coqrel.LogicalRelationsTests]
y:242 [in coqrel.RelOperators]
y:243 [in coqrel.KLR]
y:247 [in coqrel.LogicalRelationsTests]
y:25 [in coqrel.RDestruct]
y:251 [in coqrel.RelOperators]
y:254 [in coqrel.Relators]
y:259 [in coqrel.LogicalRelationsTests]
y:264 [in coqrel.RelOperators]
y:267 [in coqrel.KLR]
y:276 [in coqrel.KLR]
y:29 [in coqrel.RelQuotient]
y:32 [in coqrel.OptionRel]
y:32 [in coqrel.RDestruct]
y:34 [in coqrel.LogicalRelationsTests]
y:348 [in coqrel.RelOperators]
y:35 [in coqrel.RelClasses]
y:355 [in coqrel.RelOperators]
y:371 [in coqrel.RelOperators]
y:374 [in coqrel.RelOperators]
y:387 [in coqrel.RelOperators]
y:39 [in coqrel.KLR]
y:396 [in coqrel.RelOperators]
y:399 [in coqrel.RelOperators]
y:412 [in coqrel.RelOperators]
y:43 [in coqrel.KLR]
y:5 [in coqrel.RelClasses]
y:50 [in coqrel.LogicalRelationsTests]
y:53 [in coqrel.RelOperators]
y:55 [in coqrel.OptionRel]
y:55 [in coqrel.KLR]
y:6 [in coqrel.RelOperators]
y:60 [in coqrel.KLR]
y:61 [in coqrel.RelOperators]
y:62 [in coqrel.OptionRel]
y:64 [in coqrel.LogicalRelationsTests]
y:7 [in coqrel.OptionRel]
y:71 [in coqrel.LogicalRelationsTests]
y:75 [in coqrel.KLR]
y:8 [in coqrel.OptionRel]
y:81 [in coqrel.KLR]
y:81 [in coqrel.LogicalRelationsTests]
y:84 [in coqrel.LogicalRelationsTests]
y:86 [in coqrel.Monotonicity]
y:89 [in coqrel.LogicalRelationsTests]
y:9 [in coqrel.RDestruct]
Z
z:154 [in coqrel.RelOperators]z:19 [in coqrel.RelClasses]
z:202 [in coqrel.LogicalRelationsTests]
z:26 [in coqrel.LogicalRelationsTests]
z:260 [in coqrel.LogicalRelationsTests]
z:34 [in coqrel.RelClasses]
z:72 [in coqrel.LogicalRelationsTests]
Module Index
D
Delay [in coqrel.Delay]Library Index
B
BoolRelD
DelayK
KLRL
LogicalRelationsLogicalRelationsTests
M
MonotonicityMorphismsInterop
O
OptionRelP
PreOrderTacticR
RDestructRelators
RelClasses
RelDefinitions
RelOperators
RelQuotient
T
TransportConstructor Index
C
candidate_related [in coqrel.Monotonicity]cons_rel_def [in coqrel.Relators]
convertible [in coqrel.RelDefinitions]
coreflexivity [in coqrel.RelClasses]
E
eapply [in coqrel.Delay]I
inl_rel_def [in coqrel.Relators]inr_rel_def [in coqrel.Relators]
K
klr_inr [in coqrel.KLR]klr_inl [in coqrel.KLR]
L
left_le [in coqrel.BoolRel]left_rel_def [in coqrel.BoolRel]
M
monotonicity [in coqrel.Monotonicity]N
nil_rel_def [in coqrel.Relators]nondelayed [in coqrel.Delay]
None_ge_def [in coqrel.OptionRel]
None_le_def [in coqrel.OptionRel]
None_rel_def [in coqrel.Relators]
O
once [in coqrel.RelDefinitions]P
psat_intro [in coqrel.RelOperators]R
rauto [in coqrel.RelDefinitions]rauto_subgoals [in coqrel.RelDefinitions]
rcompose [in coqrel.RelClasses]
rdecompose [in coqrel.RelClasses]
rdestruct [in coqrel.RelDefinitions]
rdestruct_remember_intro [in coqrel.RDestruct]
related [in coqrel.RelDefinitions]
relim [in coqrel.RelDefinitions]
rel_push_rintro [in coqrel.RelOperators]
req_intro [in coqrel.RelOperators]
rexists [in coqrel.RelDefinitions]
rgraph_queue_cons [in coqrel.PreOrderTactic]
rgraph_queue_nil [in coqrel.PreOrderTactic]
right_le [in coqrel.BoolRel]
right_rel_def [in coqrel.BoolRel]
rimpl [in coqrel.Monotonicity]
rintro [in coqrel.RelDefinitions]
rstep [in coqrel.RelDefinitions]
S
Some_ge_def [in coqrel.OptionRel]Some_le_def [in coqrel.OptionRel]
Some_rel_def [in coqrel.Relators]
subrel_monotonicity [in coqrel.Monotonicity]
T
transport [in coqrel.Transport]tt_rel [in coqrel.Relators]
U
unconvertible [in coqrel.RelDefinitions]unfold_uncurry_before_after [in coqrel.RelOperators]
Lemma Index
A
arrow_pointwise_refl [in coqrel.Relators]arrow_pointwise_relim [in coqrel.Relators]
arrow_pointwise_rintro [in coqrel.Relators]
arrow_relim [in coqrel.RelDefinitions]
arrow_rintro [in coqrel.RelDefinitions]
D
direct_rexists [in coqrel.RelDefinitions]E
eqcl_reflection [in coqrel.RelQuotient]eqcl_surjective [in coqrel.RelQuotient]
F
false_leb [in coqrel.BoolRel]flip_rexists [in coqrel.RelDefinitions]
flip_rdestruct [in coqrel.RelDefinitions]
flip_relim [in coqrel.RelDefinitions]
flip_rintro [in coqrel.RelDefinitions]
flip_context_candidate [in coqrel.Monotonicity]
fold_impl_rstep [in coqrel.Relators]
forallp_relim [in coqrel.Relators]
forallp_rintro [in coqrel.Relators]
forall_pointwise_relim [in coqrel.Relators]
forall_pointwise_rintro [in coqrel.Relators]
forall_relim [in coqrel.RelDefinitions]
forall_rintro [in coqrel.RelDefinitions]
forall_relation_relim [in coqrel.MorphismsInterop]
forall_relation_rintro [in coqrel.MorphismsInterop]
f_equal_relim [in coqrel.Monotonicity]
I
impl_transport [in coqrel.Transport]K
klr_pullw_relim [in coqrel.KLR]klr_pullw_rintro [in coqrel.KLR]
klr_diam_relim [in coqrel.KLR]
klr_diam_rintro [in coqrel.KLR]
klr_box_relim [in coqrel.KLR]
klr_box_rintro [in coqrel.KLR]
k_relim [in coqrel.KLR]
k_rintro [in coqrel.KLR]
k1_relim [in coqrel.KLR]
k1_rintro [in coqrel.KLR]
k2_relim [in coqrel.KLR]
k2_rintro [in coqrel.KLR]
L
leb_rdestruct [in coqrel.BoolRel]list_rel_trans [in coqrel.Relators]
list_rel_sym [in coqrel.Relators]
list_rel_corefl [in coqrel.Relators]
list_rel_refl [in coqrel.Relators]
N
None_ge [in coqrel.OptionRel]None_le [in coqrel.OptionRel]
O
option_ge_trans [in coqrel.OptionRel]option_ge_refl [in coqrel.OptionRel]
option_le_trans [in coqrel.OptionRel]
option_le_refl [in coqrel.OptionRel]
option_rel_some_inv [in coqrel.Relators]
option_rel_refl [in coqrel.Relators]
P
pointwise_relation_relim [in coqrel.MorphismsInterop]pointwise_relation_rintro [in coqrel.MorphismsInterop]
prod_rel_preorder [in coqrel.Relators]
prod_rel_sym [in coqrel.Relators]
prod_rel_trans [in coqrel.Relators]
prod_rel_corefl [in coqrel.Relators]
prod_rel_refl [in coqrel.Relators]
psat_corefl [in coqrel.RelOperators]
Q
query_params_both [in coqrel.Monotonicity]query_params_one [in coqrel.Monotonicity]
R
rdestruct_remember_rintro [in coqrel.RDestruct]rdestruct_forget_rintro [in coqrel.RDestruct]
rdestruct_rstep [in coqrel.RDestruct]
reflexivity_rstep [in coqrel.RelDefinitions]
rel_curry2_set_le_transport [in coqrel.Transport]
rel_curry_set_le_transport [in coqrel.Transport]
rel_kvd_relim [in coqrel.KLR]
rel_kvd_rintro [in coqrel.KLR]
rel_incr_rdestruct [in coqrel.RelOperators]
rel_incr_rintro [in coqrel.RelOperators]
rel_ex_relim [in coqrel.RelOperators]
rel_ex_rintro [in coqrel.RelOperators]
rel_all_relim [in coqrel.RelOperators]
rel_all_rintro [in coqrel.RelOperators]
rel_curry_relim [in coqrel.RelOperators]
rel_push_snd_rexists [in coqrel.RelOperators]
rel_push_fst_rexists [in coqrel.RelOperators]
rel_push_corefl [in coqrel.RelOperators]
rel_pull_relim [in coqrel.RelOperators]
rel_pull_rintro [in coqrel.RelOperators]
rel_pull_rcompose [in coqrel.RelOperators]
rel_pull_sym [in coqrel.RelOperators]
rel_pull_refl [in coqrel.RelOperators]
rel_compose_assoc [in coqrel.RelOperators]
rel_compose_id_right [in coqrel.RelOperators]
rel_compose_id_left [in coqrel.RelOperators]
rel_top_rintro [in coqrel.RelOperators]
rel_bot_relim [in coqrel.RelOperators]
rel_bot_subrel [in coqrel.RelOperators]
rel_impl_subrel_codomain [in coqrel.RelOperators]
rel_impl_relim [in coqrel.RelOperators]
rel_impl_rintro [in coqrel.RelOperators]
rel_inter_sym [in coqrel.RelOperators]
rel_inter_trans [in coqrel.RelOperators]
rel_inter_corefl_r [in coqrel.RelOperators]
rel_inter_corefl_l [in coqrel.RelOperators]
rel_inter_refl [in coqrel.RelOperators]
rel_inter_glb [in coqrel.RelOperators]
rel_inter_subrel_rexists_r [in coqrel.RelOperators]
rel_inter_subrel_rexists_l [in coqrel.RelOperators]
rel_inter_rexists [in coqrel.RelOperators]
rel_union_sym [in coqrel.RelOperators]
rel_union_corefl [in coqrel.RelOperators]
rel_union_refl_r [in coqrel.RelOperators]
rel_union_refl_l [in coqrel.RelOperators]
rel_union_lub [in coqrel.RelOperators]
rel_union_subrel_rexists_r [in coqrel.RelOperators]
rel_union_subrel_rexists_l [in coqrel.RelOperators]
rel_union_rexists_r [in coqrel.RelOperators]
rel_union_rexists_l [in coqrel.RelOperators]
rel_top_component_trsym [in coqrel.LogicalRelationsTests]
rel_top_component_refl [in coqrel.LogicalRelationsTests]
rel_ex_1 [in coqrel.LogicalRelationsTests]
rel_all_1 [in coqrel.LogicalRelationsTests]
rel_pull_2 [in coqrel.LogicalRelationsTests]
req_corefl [in coqrel.RelOperators]
req_rintro [in coqrel.RelOperators]
respectful_relim [in coqrel.MorphismsInterop]
respectful_rintro [in coqrel.MorphismsInterop]
S
set_le_transport [in coqrel.Transport]set_ge_refl [in coqrel.Relators]
set_le_refl [in coqrel.Relators]
subrelation_subrel [in coqrel.MorphismsInterop]
subrel_sym_flip [in coqrel.RelOperators]
sum_rel_preorder [in coqrel.Relators]
sum_rel_sym [in coqrel.Relators]
sum_rel_trans [in coqrel.Relators]
sum_rel_corefl [in coqrel.Relators]
sum_rel_refl [in coqrel.Relators]
T
transitive_rcompose [in coqrel.RelClasses]transport_in_goal [in coqrel.Transport]
true_leb [in coqrel.BoolRel]
U
unfold_monotonic_rstep [in coqrel.RelDefinitions]Projection Index
A
acc [in coqrel.KLR]C
candidate_related [in coqrel.Monotonicity]convertible [in coqrel.RelDefinitions]
coreflexivity [in coqrel.RelClasses]
D
Delay.open_conjunction_proj [in coqrel.Delay]E
eapply [in coqrel.Delay]I
in_eqcl_wf [in coqrel.RelQuotient]in_eqcl [in coqrel.RelQuotient]
M
monotonicity [in coqrel.Monotonicity]N
nondelayed [in coqrel.Delay]O
once [in coqrel.RelDefinitions]R
rauto [in coqrel.RelDefinitions]rauto_subgoals [in coqrel.RelDefinitions]
rcompose [in coqrel.RelClasses]
rdecompose [in coqrel.RelClasses]
rdestruct [in coqrel.RelDefinitions]
related [in coqrel.RelDefinitions]
relim [in coqrel.RelDefinitions]
rexists [in coqrel.RelDefinitions]
rimpl [in coqrel.Monotonicity]
rintro [in coqrel.RelDefinitions]
rstep [in coqrel.RelDefinitions]
S
subrel_monotonicity [in coqrel.Monotonicity]T
transport [in coqrel.Transport]U
unconvertible [in coqrel.RelDefinitions]unfold_uncurry_before_after [in coqrel.RelOperators]
Inductive Index
C
CandidateProperty [in coqrel.Monotonicity]Convertible [in coqrel.RelDefinitions]
Coreflexive [in coqrel.RelClasses]
E
EApply [in coqrel.Delay]Empty_set_rel [in coqrel.Relators]
K
klr_sum [in coqrel.KLR]L
list_rel [in coqrel.Relators]M
Monotonicity [in coqrel.Monotonicity]N
NonDelayed [in coqrel.Delay]O
Once [in coqrel.RelDefinitions]option_ge [in coqrel.OptionRel]
option_le [in coqrel.OptionRel]
option_rel [in coqrel.Relators]
P
psat [in coqrel.RelOperators]R
RAuto [in coqrel.RelDefinitions]RAutoSubgoals [in coqrel.RelDefinitions]
RCompose [in coqrel.RelClasses]
RDecompose [in coqrel.RelClasses]
RDestruct [in coqrel.RelDefinitions]
rdestruct_remember [in coqrel.RDestruct]
Related [in coqrel.RelDefinitions]
RElim [in coqrel.RelDefinitions]
rel_push [in coqrel.RelOperators]
req [in coqrel.RelOperators]
RExists [in coqrel.RelDefinitions]
rgraph_queue [in coqrel.PreOrderTactic]
RImpl [in coqrel.Monotonicity]
RIntro [in coqrel.RelDefinitions]
RStep [in coqrel.RelDefinitions]
S
SubrelMonotonicity [in coqrel.Monotonicity]sumbool_le [in coqrel.BoolRel]
sumbool_rel [in coqrel.BoolRel]
sum_rel [in coqrel.Relators]
T
Transport [in coqrel.Transport]U
Unconvertible [in coqrel.RelDefinitions]UnfoldUncurry [in coqrel.RelOperators]
unit_rel [in coqrel.Relators]
Instance Index
A
all_monotonic_params [in coqrel.Relators]all_monotonic [in coqrel.Relators]
andb_leb [in coqrel.BoolRel]
and_monotonic [in coqrel.Relators]
apply_candidate_subrel [in coqrel.Monotonicity]
apply_candidate [in coqrel.Monotonicity]
app_rel [in coqrel.Relators]
arrow_pointwise_rel_compose [in coqrel.Relators]
arrow_pointwise_subrel_params [in coqrel.Relators]
arrow_pointwise_subrel [in coqrel.Relators]
arrow_rdecompose [in coqrel.RelClasses]
arrow_rcompose [in coqrel.RelClasses]
arrow_corefl [in coqrel.RelClasses]
arrow_refl [in coqrel.RelClasses]
arrow_subrel_params [in coqrel.RelDefinitions]
arrow_subrel [in coqrel.RelDefinitions]
as_is_candidate [in coqrel.Monotonicity]
C
cons_rel [in coqrel.Relators]E
eqcl_of_eq [in coqrel.RelQuotient]eqcl_of_le [in coqrel.RelQuotient]
eqcl_le_po [in coqrel.RelQuotient]
eqcl_le_preo [in coqrel.RelQuotient]
eqcl_params [in coqrel.RelQuotient]
eqrel_subrel [in coqrel.RelOperators]
eqrel_equivalence [in coqrel.RelOperators]
eq_corefl [in coqrel.RelClasses]
eq_subrel [in coqrel.RelDefinitions]
eq_candidate [in coqrel.Monotonicity]
ex_monotonic_params [in coqrel.Relators]
ex_monotonic [in coqrel.Relators]
F
flip_subrel_params [in coqrel.RelDefinitions]flip_subrel [in coqrel.RelDefinitions]
fold_left_rel [in coqrel.Relators]
fold_right_rel [in coqrel.Relators]
forall_relation_params [in coqrel.MorphismsInterop]
forall_relation_subrel [in coqrel.MorphismsInterop]
fst_rel [in coqrel.Relators]
I
implb_leb [in coqrel.BoolRel]inl_rel [in coqrel.Relators]
inr_rel [in coqrel.Relators]
K
klr_pullw_subrel_params [in coqrel.KLR]klr_pullw_subrel [in coqrel.KLR]
klr_diam_subrel_params [in coqrel.KLR]
klr_box_subrel_params [in coqrel.KLR]
klr_diam_subrel [in coqrel.KLR]
klr_box_subrel [in coqrel.KLR]
k_rel_params [in coqrel.KLR]
k_rel [in coqrel.KLR]
k1_rel_params [in coqrel.KLR]
k1_rel [in coqrel.KLR]
k2_rel_params [in coqrel.KLR]
k2_unfold [in coqrel.KLR]
k2_rel [in coqrel.KLR]
L
leb_transport_eq_true [in coqrel.BoolRel]leb_preo [in coqrel.BoolRel]
left_rel [in coqrel.BoolRel]
length_rel [in coqrel.Relators]
list_subrel_params [in coqrel.Relators]
list_subrel [in coqrel.Relators]
lsat_subrel_params [in coqrel.RelOperators]
lsat_subrel [in coqrel.RelOperators]
M
map_rel [in coqrel.Relators]monotonicity_rstep [in coqrel.Monotonicity]
morphisms_proper_related [in coqrel.MorphismsInterop]
N
negb_leb [in coqrel.BoolRel]nil_rel [in coqrel.Relators]
None_rel [in coqrel.Relators]
O
option_ge_transport_eq_none [in coqrel.OptionRel]option_le_transport_eq_some [in coqrel.OptionRel]
option_map_ge [in coqrel.OptionRel]
option_ge_rel [in coqrel.OptionRel]
option_ge_subrel_params [in coqrel.OptionRel]
option_ge_subrel [in coqrel.OptionRel]
option_map_le [in coqrel.OptionRel]
option_le_rel [in coqrel.OptionRel]
option_le_subrel_params [in coqrel.OptionRel]
option_le_subrel [in coqrel.OptionRel]
option_map_rel [in coqrel.Relators]
option_subrel_params [in coqrel.Relators]
option_subrel [in coqrel.Relators]
orb_leb [in coqrel.BoolRel]
or_monotonic [in coqrel.Relators]
P
pair_rel [in coqrel.Relators]pointwise_relation_subrel_subrel [in coqrel.MorphismsInterop]
pointwise_relation_params [in coqrel.MorphismsInterop]
pointwise_relation_subrel [in coqrel.MorphismsInterop]
prod_rel_transport_eq_pair [in coqrel.Transport]
prod_rdestruct [in coqrel.Relators]
prod_subrel_params [in coqrel.Relators]
prod_subrel [in coqrel.Relators]
psat_subrel_params [in coqrel.RelOperators]
psat_subrel [in coqrel.RelOperators]
R
rauto_rstep [in coqrel.RelDefinitions]rcompose_transitive [in coqrel.RelClasses]
rcompose_subrel [in coqrel.RelOperators]
rdecompose_subrel [in coqrel.RelOperators]
relim_base [in coqrel.RelDefinitions]
rel_kvd_subrel_params [in coqrel.KLR]
rel_kvd_subrel [in coqrel.KLR]
rel_incr_subrel_params [in coqrel.RelOperators]
rel_incr_subrel [in coqrel.RelOperators]
rel_push_subrel_params [in coqrel.RelOperators]
rel_push_subrel [in coqrel.RelOperators]
rel_pull_subrel_params [in coqrel.RelOperators]
rel_pull_subrel [in coqrel.RelOperators]
rel_compose_rdecompose [in coqrel.RelOperators]
rel_compose_rcompose [in coqrel.RelOperators]
rel_compose_params [in coqrel.RelOperators]
rel_compose_eqrel [in coqrel.RelOperators]
rel_compose_subrel [in coqrel.RelOperators]
rel_top_equiv [in coqrel.RelOperators]
rel_impl_subrel_params [in coqrel.RelOperators]
rel_impl_subrel [in coqrel.RelOperators]
rel_inter_flip_sym [in coqrel.RelOperators]
rel_inter_params [in coqrel.RelOperators]
rel_inter_subrel [in coqrel.RelOperators]
rel_union_subrel_params [in coqrel.RelOperators]
rel_union_subrel [in coqrel.RelOperators]
remove_all_params_candidate [in coqrel.Monotonicity]
remove_params_candidate [in coqrel.Monotonicity]
respectful_params [in coqrel.MorphismsInterop]
respectful_subrel [in coqrel.MorphismsInterop]
rexists_rstep [in coqrel.RelDefinitions]
right_rel [in coqrel.BoolRel]
rimpl_flip_subrel [in coqrel.Monotonicity]
rimpl_subrel [in coqrel.Monotonicity]
rimpl_refl [in coqrel.Monotonicity]
rintro_rstep [in coqrel.RelDefinitions]
rsat_subrel_params [in coqrel.RelOperators]
rsat_subrel [in coqrel.RelOperators]
S
set_ge_compose [in coqrel.Relators]set_ge_subrel_params [in coqrel.Relators]
set_ge_subrel [in coqrel.Relators]
set_le_compose [in coqrel.Relators]
set_le_subrel_params [in coqrel.Relators]
set_le_subrel [in coqrel.Relators]
snd_rel [in coqrel.Relators]
Some_ge [in coqrel.OptionRel]
Some_le [in coqrel.OptionRel]
Some_rel [in coqrel.Relators]
subrel_eq [in coqrel.RelClasses]
subrel_impl_relim [in coqrel.RelDefinitions]
subrel_preorder [in coqrel.RelDefinitions]
sum_subrel_params [in coqrel.Relators]
sum_subrel [in coqrel.Relators]
Section Index
A
ARROW_REL_COMPOSE [in coqrel.RelClasses]ARROW_MOD [in coqrel.KLR]
L
LIFT [in coqrel.KLR]M
MODALITIES [in coqrel.KLR]P
PROPERTIES [in coqrel.RelQuotient]U
UNKRIPKIFY [in coqrel.KLR]USUAL [in coqrel.KLR]
Abbreviation Index
M
Monotonic [in coqrel.RelDefinitions]Record Index
C
CandidateProperty [in coqrel.Monotonicity]CommonPrefix [in coqrel.Monotonicity]
Convertible [in coqrel.RelDefinitions]
Coreflexive [in coqrel.RelClasses]
D
Delay.open_conjunction [in coqrel.Delay]E
EApply [in coqrel.Delay]K
KripkeFrame [in coqrel.KLR]M
Monotonicity [in coqrel.Monotonicity]N
NonDelayed [in coqrel.Delay]NotEvar [in coqrel.RelDefinitions]
O
Once [in coqrel.RelDefinitions]P
PolarityResolved [in coqrel.RelDefinitions]Q
QueryParams [in coqrel.Monotonicity]quotient [in coqrel.RelQuotient]
R
RAuto [in coqrel.RelDefinitions]RAutoSubgoals [in coqrel.RelDefinitions]
RCompose [in coqrel.RelClasses]
RDecompose [in coqrel.RelClasses]
RDestruct [in coqrel.RelDefinitions]
Related [in coqrel.RelDefinitions]
RElim [in coqrel.RelDefinitions]
RemoveAllParams [in coqrel.Monotonicity]
RemoveParams [in coqrel.Monotonicity]
RExists [in coqrel.RelDefinitions]
RImpl [in coqrel.Monotonicity]
RIntro [in coqrel.RelDefinitions]
RStep [in coqrel.RelDefinitions]
S
SubrelMonotonicity [in coqrel.Monotonicity]T
Transport [in coqrel.Transport]U
Unconvertible [in coqrel.RelDefinitions]UnfoldUncurry [in coqrel.RelOperators]
Definition Index
A
arrow_pointwise_rel [in coqrel.Relators]arrow_pointwise_klr [in coqrel.KLR]
arrow_klr [in coqrel.KLR]
arrow_rel [in coqrel.RelDefinitions]
C
curry [in coqrel.RelOperators]D
delay [in coqrel.Delay]Delay.delayed_goal [in coqrel.Delay]
Delay.unpack [in coqrel.Delay]
E
eqcl [in coqrel.RelQuotient]eqrel [in coqrel.RelOperators]
F
forallp_rel [in coqrel.Relators]forall_pointwise_rel [in coqrel.Relators]
forall_rel [in coqrel.RelDefinitions]
K
k [in coqrel.KLR]klr [in coqrel.KLR]
klr_pullw [in coqrel.KLR]
klr_diamat [in coqrel.KLR]
klr_boxto [in coqrel.KLR]
klr_diam [in coqrel.KLR]
klr_box [in coqrel.KLR]
klr_curry [in coqrel.KLR]
klr_inter [in coqrel.KLR]
klr_union [in coqrel.KLR]
k1 [in coqrel.KLR]
k2 [in coqrel.KLR]
L
list_klr [in coqrel.KLR]lsat [in coqrel.RelOperators]
P
prod_rel [in coqrel.Relators]prod_klr [in coqrel.KLR]
Q
qle [in coqrel.RelQuotient]R
rdestruct_result [in coqrel.RDestruct]rel [in coqrel.RelDefinitions]
rel_kvd [in coqrel.KLR]
rel_incr [in coqrel.RelOperators]
rel_ex [in coqrel.RelOperators]
rel_all [in coqrel.RelOperators]
rel_uncurry [in coqrel.RelOperators]
rel_curry [in coqrel.RelOperators]
rel_pull [in coqrel.RelOperators]
rel_compose [in coqrel.RelOperators]
rel_top [in coqrel.RelOperators]
rel_bot [in coqrel.RelOperators]
rel_impl [in coqrel.RelOperators]
rel_inter [in coqrel.RelOperators]
rel_union [in coqrel.RelOperators]
rgraph_done [in coqrel.PreOrderTactic]
rsat [in coqrel.RelOperators]
S
set_ge [in coqrel.Relators]set_le [in coqrel.Relators]
set_kge [in coqrel.KLR]
set_kle [in coqrel.KLR]
subrel [in coqrel.RelDefinitions]
sum_klr [in coqrel.KLR]
U
uncurry [in coqrel.RelOperators]Unnamed_thm26 [in coqrel.LogicalRelationsTests]
Unnamed_thm25 [in coqrel.LogicalRelationsTests]
Unnamed_thm24 [in coqrel.LogicalRelationsTests]
Unnamed_thm24 [in coqrel.LogicalRelationsTests]
Unnamed_thm23 [in coqrel.LogicalRelationsTests]
Unnamed_thm22 [in coqrel.LogicalRelationsTests]
Unnamed_thm21 [in coqrel.LogicalRelationsTests]
Unnamed_thm20 [in coqrel.LogicalRelationsTests]
Unnamed_thm19 [in coqrel.LogicalRelationsTests]
Unnamed_thm18 [in coqrel.LogicalRelationsTests]
Unnamed_thm17 [in coqrel.LogicalRelationsTests]
Unnamed_thm16 [in coqrel.LogicalRelationsTests]
Unnamed_thm15 [in coqrel.LogicalRelationsTests]
Unnamed_thm14 [in coqrel.LogicalRelationsTests]
Unnamed_thm13 [in coqrel.LogicalRelationsTests]
Unnamed_thm13 [in coqrel.LogicalRelationsTests]
Unnamed_thm12 [in coqrel.LogicalRelationsTests]
Unnamed_thm11 [in coqrel.LogicalRelationsTests]
Unnamed_thm11 [in coqrel.LogicalRelationsTests]
Unnamed_thm10 [in coqrel.LogicalRelationsTests]
Unnamed_thm9 [in coqrel.LogicalRelationsTests]
Unnamed_thm8 [in coqrel.LogicalRelationsTests]
Unnamed_thm7 [in coqrel.LogicalRelationsTests]
Unnamed_thm7 [in coqrel.LogicalRelationsTests]
Unnamed_thm6 [in coqrel.LogicalRelationsTests]
Unnamed_thm5 [in coqrel.LogicalRelationsTests]
Unnamed_thm4 [in coqrel.LogicalRelationsTests]
Unnamed_thm3 [in coqrel.LogicalRelationsTests]
Unnamed_thm2 [in coqrel.LogicalRelationsTests]
Unnamed_thm1 [in coqrel.LogicalRelationsTests]
Unnamed_thm0 [in coqrel.LogicalRelationsTests]
Unnamed_thm [in coqrel.LogicalRelationsTests]
Unnamed_thm [in coqrel.LogicalRelationsTests]
| 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 | (2458 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 | (47 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 | (1882 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| 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 | (45 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 | (133 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (26 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 | (37 entries) |
| Instance 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 | (145 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 | (7 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (31 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 | (87 entries) |
This page has been generated by coqdoc