| 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 | (75519 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 | (245 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 | (61331 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 | (144 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (89 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (236 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 | (6913 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 | (1141 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (34 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 | (269 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 | (443 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 | (296 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 | (604 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 | (248 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 | (3386 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (140 entries) |
R (binder)
rangsort:226 [in MetaCoq.Template.Universes]rangsort:294 [in MetaCoq.Template.Universes]
rarg:144 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
rarg:156 [in MetaCoq.PCUIC.PCUICWcbvEval]
rarg:157 [in MetaCoq.Erasure.EWcbvEval]
rarg:23 [in MetaCoq.PCUIC.PCUICInductiveInversion]
rarg:246 [in MetaCoq.PCUIC.PCUICNormal]
rarg:257 [in MetaCoq.PCUIC.PCUICNormal]
rarg:257 [in MetaCoq.Template.WcbvEval]
rarg:267 [in MetaCoq.PCUIC.PCUICNormal]
rarg:340 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
rarg:343 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
rarg:61 [in MetaCoq.PCUIC.PCUICNormal]
ra:1001 [in MetaCoq.PCUIC.PCUICReduction]
ra:1022 [in MetaCoq.PCUIC.PCUICReduction]
ra:1027 [in MetaCoq.PCUIC.PCUICReduction]
ra:1067 [in MetaCoq.PCUIC.PCUICReduction]
ra:1072 [in MetaCoq.PCUIC.PCUICReduction]
ra:1093 [in MetaCoq.PCUIC.PCUICReduction]
ra:1098 [in MetaCoq.PCUIC.PCUICReduction]
ra:1765 [in MetaCoq.SafeChecker.PCUICSafeConversion]
ra:19 [in MetaCoq.PCUIC.Syntax.PCUICReflect]
ra:28 [in MetaCoq.PCUIC.Syntax.PCUICReflect]
ra:39 [in MetaCoq.PCUIC.Syntax.PCUICReflect]
ra:47 [in MetaCoq.PCUIC.Syntax.PCUICReflect]
RA:53 [in MetaCoq.PCUIC.utils.PCUICUtils]
RA:72 [in MetaCoq.Template.utils.ReflectEq]
ra:996 [in MetaCoq.PCUIC.PCUICReduction]
rb:20 [in MetaCoq.PCUIC.Syntax.PCUICReflect]
rb:29 [in MetaCoq.PCUIC.Syntax.PCUICReflect]
RB:54 [in MetaCoq.PCUIC.utils.PCUICUtils]
rctx:1154 [in MetaCoq.PCUIC.PCUICConfluence]
rctx:1159 [in MetaCoq.PCUIC.PCUICConfluence]
rc:30 [in MetaCoq.PCUIC.Syntax.PCUICReflect]
rd:29 [in MetaCoq.Template.TemplateMonad.Extractable]
rd:33 [in MetaCoq.Template.TemplateMonad.Extractable]
rd:38 [in MetaCoq.Template.TemplateMonad.Extractable]
rd:43 [in MetaCoq.Template.TemplateMonad.Core]
rd:43 [in MetaCoq.Template.TemplateMonad.Extractable]
redctx:1170 [in MetaCoq.PCUIC.PCUICConfluence]
redctx:1214 [in MetaCoq.PCUIC.PCUICConfluence]
redt:257 [in MetaCoq.Template.Checker]
redt:259 [in MetaCoq.Template.Checker]
redt:272 [in MetaCoq.Template.Checker]
redt:274 [in MetaCoq.Template.Checker]
reduce:356 [in MetaCoq.SafeChecker.PCUICSafeReduce]
red1:244 [in MetaCoq.Template.Checker]
red2:245 [in MetaCoq.Template.Checker]
red:646 [in MetaCoq.PCUIC.PCUICReduction]
red:7 [in MetaCoq.Template.TemplateMonad.Extractable]
refl':556 [in MetaCoq.PCUIC.PCUICConfluence]
refl:555 [in MetaCoq.PCUIC.PCUICConfluence]
ref:100 [in MetaCoq.SafeChecker.PCUICWfEnv]
ref:1111 [in MetaCoq.PCUIC.PCUICConversion]
ref:117 [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
ref:132 [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
ref:157 [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
ref:161 [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
ref:164 [in MetaCoq.SafeChecker.PCUICEqualityDec]
ref:167 [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
ref:178 [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
ref:217 [in MetaCoq.SafeChecker.PCUICEqualityDec]
ref:240 [in MetaCoq.SafeChecker.PCUICEqualityDec]
ref:255 [in MetaCoq.SafeChecker.PCUICEqualityDec]
ref:274 [in MetaCoq.SafeChecker.PCUICEqualityDec]
ref:279 [in MetaCoq.SafeChecker.PCUICEqualityDec]
ref:329 [in MetaCoq.SafeChecker.PCUICEqualityDec]
ref:355 [in MetaCoq.SafeChecker.PCUICEqualityDec]
ref:371 [in MetaCoq.SafeChecker.PCUICEqualityDec]
ref:376 [in MetaCoq.SafeChecker.PCUICEqualityDec]
ref:381 [in MetaCoq.SafeChecker.PCUICEqualityDec]
ref:58 [in MetaCoq.PCUIC.PCUICPrincipality]
ref:87 [in MetaCoq.SafeChecker.PCUICEqualityDec]
ref:92 [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
ref:94 [in MetaCoq.SafeChecker.PCUICEqualityDec]
relx:88 [in MetaCoq.PCUIC.Syntax.PCUICReflect]
rely:92 [in MetaCoq.PCUIC.Syntax.PCUICReflect]
rel:11 [in MetaCoq.PCUIC.PCUICParallelReduction]
rel:16 [in MetaCoq.PCUIC.PCUICParallelReduction]
rel:168 [in MetaCoq.PCUIC.PCUICSafeLemmata]
rel:175 [in MetaCoq.PCUIC.PCUICSafeLemmata]
rel:254 [in MetaCoq.PCUIC.PCUICSafeLemmata]
rel:263 [in MetaCoq.PCUIC.PCUICSafeLemmata]
rel:58 [in MetaCoq.PCUIC.PCUICParallelReduction]
rel:69 [in MetaCoq.PCUIC.PCUICParallelReduction]
rel:780 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
remaining_subst:10 [in MetaCoq.Template.EtaExpand]
remaining:9 [in MetaCoq.Template.EtaExpand]
Req:1109 [in MetaCoq.PCUIC.PCUICConversion]
res:101 [in MetaCoq.Template.WcbvEval]
res:102 [in MetaCoq.Erasure.EWcbvEval]
res:104 [in MetaCoq.Erasure.EWcbvEvalInd]
res:107 [in MetaCoq.Erasure.EWcbvEval]
res:112 [in MetaCoq.Erasure.EWcbvEvalInd]
res:113 [in MetaCoq.Erasure.EWcbvEval]
res:114 [in MetaCoq.Template.Checker]
res:116 [in MetaCoq.Erasure.EWcbvEvalInd]
res:117 [in MetaCoq.PCUIC.PCUICWcbvEval]
res:119 [in MetaCoq.Template.WcbvEval]
res:119 [in MetaCoq.Erasure.EWcbvEval]
res:122 [in MetaCoq.Erasure.EWcbvEvalInd]
res:125 [in MetaCoq.PCUIC.PCUICWcbvEval]
res:127 [in MetaCoq.Template.WcbvEval]
res:134 [in MetaCoq.Erasure.EWcbvEvalInd]
res:147 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
res:150 [in MetaCoq.Template.WcbvEval]
res:152 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
res:156 [in MetaCoq.Template.WcbvEval]
res:161 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
res:161 [in MetaCoq.Template.WcbvEval]
res:169 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
res:173 [in MetaCoq.Template.WcbvEval]
res:177 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
res:186 [in MetaCoq.Template.WcbvEval]
res:19 [in MetaCoq.Erasure.EWcbvEvalInd]
res:193 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
res:195 [in MetaCoq.Template.WcbvEval]
res:202 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
res:210 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
res:213 [in MetaCoq.Template.WcbvEval]
res:214 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
res:220 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
res:221 [in MetaCoq.Template.WcbvEval]
res:25 [in MetaCoq.Erasure.EWcbvEvalInd]
res:28 [in MetaCoq.Erasure.EWcbvEval]
res:326 [in MetaCoq.Erasure.EArities]
res:33 [in MetaCoq.Erasure.EWcbvEval]
res:34 [in MetaCoq.Erasure.EWcbvEvalInd]
res:42 [in MetaCoq.Erasure.EWcbvEval]
res:50 [in MetaCoq.Erasure.EWcbvEvalInd]
res:51 [in MetaCoq.Erasure.EWcbvEval]
res:535 [in MetaCoq.Erasure.EEtaExpandedFix]
res:541 [in MetaCoq.Erasure.EEtaExpandedFix]
res:546 [in MetaCoq.Erasure.EEtaExpandedFix]
res:57 [in MetaCoq.PCUIC.PCUICWcbvEval]
res:57 [in MetaCoq.Template.WcbvEval]
res:58 [in MetaCoq.Erasure.EWcbvEval]
res:6 [in MetaCoq.Erasure.EEtaExpandedFix]
res:61 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
res:63 [in MetaCoq.PCUIC.PCUICWcbvEval]
res:63 [in MetaCoq.Template.WcbvEval]
res:64 [in MetaCoq.Erasure.EWcbvEvalInd]
res:66 [in MetaCoq.Template.Checker]
res:66 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
res:66 [in MetaCoq.Erasure.EWcbvEval]
res:69 [in MetaCoq.PCUIC.PCUICWcbvEval]
res:69 [in MetaCoq.Template.WcbvEval]
res:7 [in MetaCoq.PCUIC.PCUICProgress]
res:70 [in MetaCoq.Template.Checker]
res:72 [in MetaCoq.Erasure.EWcbvEvalInd]
res:75 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
res:77 [in MetaCoq.Template.Checker]
res:81 [in MetaCoq.PCUIC.PCUICWcbvEval]
res:81 [in MetaCoq.Template.WcbvEval]
res:83 [in MetaCoq.Template.Checker]
res:83 [in MetaCoq.Erasure.EWcbvEval]
res:87 [in MetaCoq.PCUIC.PCUICWcbvEval]
res:88 [in MetaCoq.Template.WcbvEval]
res:89 [in MetaCoq.Template.Checker]
res:91 [in MetaCoq.Erasure.EWcbvEvalInd]
res:923 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
res:94 [in MetaCoq.Erasure.EWcbvEval]
res:99 [in MetaCoq.PCUIC.PCUICWcbvEval]
ret_binders:73 [in MetaCoq.Template.Pretty]
ret_binders:80 [in MetaCoq.PCUIC.utils.PCUICPretty]
ret':643 [in MetaCoq.PCUIC.PCUICSR]
ret:189 [in MetaCoq.PCUIC.PCUICAlpha]
ret:199 [in MetaCoq.PCUIC.PCUICAlpha]
ret:642 [in MetaCoq.PCUIC.PCUICSR]
Re':175 [in MetaCoq.Template.TermEquality]
Re':182 [in MetaCoq.Template.TermEquality]
Re':191 [in MetaCoq.Template.TermEquality]
Re':210 [in MetaCoq.Template.TermEquality]
Re':218 [in MetaCoq.Template.TermEquality]
Re':247 [in MetaCoq.PCUIC.PCUICContextConversion]
Re':337 [in MetaCoq.PCUIC.PCUICEquality]
Re':344 [in MetaCoq.PCUIC.PCUICEquality]
Re':355 [in MetaCoq.PCUIC.PCUICEquality]
Re':370 [in MetaCoq.PCUIC.PCUICEquality]
Re':377 [in MetaCoq.PCUIC.PCUICEquality]
Re':45 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
Re':53 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
Re':637 [in MetaCoq.PCUIC.PCUICEquality]
Re:10 [in MetaCoq.Template.TermEquality]
Re:105 [in MetaCoq.PCUIC.PCUICAlpha]
Re:1115 [in MetaCoq.PCUIC.PCUICConversion]
Re:112 [in MetaCoq.PCUIC.PCUICEquality]
Re:116 [in MetaCoq.PCUIC.PCUICEquality]
Re:120 [in MetaCoq.PCUIC.PCUICConfluence]
Re:122 [in MetaCoq.SafeChecker.PCUICEqualityDec]
Re:14 [in MetaCoq.PCUIC.PCUICEquality]
Re:142 [in MetaCoq.PCUIC.PCUICConfluence]
Re:151 [in MetaCoq.Template.TermEquality]
Re:152 [in MetaCoq.SafeChecker.PCUICEqualityDec]
Re:161 [in MetaCoq.Template.TermEquality]
Re:173 [in MetaCoq.PCUIC.PCUICContextConversion]
Re:174 [in MetaCoq.Template.TermEquality]
Re:181 [in MetaCoq.Template.TermEquality]
Re:187 [in MetaCoq.PCUIC.PCUICContextConversion]
Re:19 [in MetaCoq.PCUIC.PCUICAlpha]
Re:190 [in MetaCoq.Template.TermEquality]
Re:190 [in MetaCoq.SafeChecker.PCUICEqualityDec]
Re:205 [in MetaCoq.SafeChecker.PCUICEqualityDec]
Re:209 [in MetaCoq.Template.TermEquality]
Re:217 [in MetaCoq.Template.TermEquality]
Re:218 [in MetaCoq.PCUIC.PCUICEquality]
Re:225 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
Re:229 [in MetaCoq.PCUIC.PCUICEquality]
Re:229 [in MetaCoq.SafeChecker.PCUICEqualityDec]
Re:230 [in MetaCoq.Template.TermEquality]
Re:230 [in MetaCoq.PCUIC.PCUICEquality]
Re:231 [in MetaCoq.PCUIC.PCUICEquality]
Re:233 [in MetaCoq.PCUIC.PCUICAlpha]
Re:237 [in MetaCoq.PCUIC.PCUICEquality]
Re:238 [in MetaCoq.PCUIC.PCUICAlpha]
Re:240 [in MetaCoq.PCUIC.PCUICEquality]
Re:242 [in MetaCoq.Template.TermEquality]
Re:245 [in MetaCoq.PCUIC.PCUICContextConversion]
Re:248 [in MetaCoq.PCUIC.PCUICEquality]
Re:261 [in MetaCoq.PCUIC.PCUICEquality]
Re:264 [in MetaCoq.PCUIC.PCUICEquality]
Re:269 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
Re:27 [in MetaCoq.PCUIC.PCUICEquality]
Re:270 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
Re:270 [in MetaCoq.PCUIC.PCUICEquality]
Re:277 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
Re:282 [in MetaCoq.PCUIC.PCUICEquality]
Re:285 [in MetaCoq.PCUIC.PCUICEquality]
Re:285 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
Re:287 [in MetaCoq.PCUIC.PCUICConfluence]
Re:288 [in MetaCoq.PCUIC.PCUICCumulProp]
Re:29 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
Re:293 [in MetaCoq.PCUIC.PCUICEquality]
Re:293 [in MetaCoq.PCUIC.PCUICConfluence]
Re:294 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
Re:296 [in MetaCoq.PCUIC.PCUICConversion]
Re:299 [in MetaCoq.PCUIC.PCUICConfluence]
Re:3 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
Re:30 [in MetaCoq.Template.TermEquality]
Re:300 [in MetaCoq.SafeChecker.PCUICEqualityDec]
Re:301 [in MetaCoq.PCUIC.PCUICConversion]
Re:308 [in MetaCoq.SafeChecker.PCUICEqualityDec]
Re:309 [in MetaCoq.PCUIC.PCUICEquality]
Re:317 [in MetaCoq.PCUIC.PCUICConfluence]
Re:317 [in MetaCoq.SafeChecker.PCUICEqualityDec]
Re:318 [in MetaCoq.PCUIC.PCUICEquality]
Re:32 [in MetaCoq.PCUIC.PCUICEquality]
Re:322 [in MetaCoq.PCUIC.PCUICContextConversion]
Re:324 [in MetaCoq.PCUIC.PCUICEquality]
Re:327 [in MetaCoq.PCUIC.PCUICConfluence]
Re:327 [in MetaCoq.PCUIC.PCUICContextConversion]
Re:335 [in MetaCoq.PCUIC.PCUICConfluence]
Re:336 [in MetaCoq.PCUIC.PCUICEquality]
Re:34 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
Re:341 [in MetaCoq.PCUIC.PCUICConfluence]
Re:343 [in MetaCoq.PCUIC.PCUICEquality]
Re:347 [in MetaCoq.SafeChecker.PCUICEqualityDec]
Re:349 [in MetaCoq.PCUIC.PCUICConfluence]
Re:35 [in MetaCoq.Template.TermEquality]
Re:354 [in MetaCoq.PCUIC.PCUICEquality]
Re:36 [in MetaCoq.PCUIC.PCUICSafeLemmata]
Re:369 [in MetaCoq.PCUIC.PCUICEquality]
Re:374 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
Re:376 [in MetaCoq.PCUIC.PCUICEquality]
Re:38 [in MetaCoq.PCUIC.PCUICSafeLemmata]
Re:38 [in MetaCoq.PCUIC.PCUICAlpha]
Re:383 [in MetaCoq.PCUIC.PCUICEquality]
Re:384 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
Re:4 [in MetaCoq.Template.TermEquality]
Re:402 [in MetaCoq.PCUIC.PCUICEquality]
Re:42 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
Re:44 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
Re:456 [in MetaCoq.PCUIC.PCUICEquality]
Re:465 [in MetaCoq.PCUIC.PCUICEquality]
Re:47 [in MetaCoq.PCUIC.PCUICSN]
Re:48 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
Re:485 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
Re:487 [in MetaCoq.PCUIC.PCUICEquality]
Re:493 [in MetaCoq.PCUIC.PCUICEquality]
Re:499 [in MetaCoq.PCUIC.PCUICEquality]
Re:507 [in MetaCoq.PCUIC.PCUICEquality]
Re:516 [in MetaCoq.PCUIC.PCUICEquality]
Re:52 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
Re:523 [in MetaCoq.PCUIC.PCUICConfluence]
Re:525 [in MetaCoq.PCUIC.PCUICEquality]
Re:527 [in MetaCoq.PCUIC.PCUICNormal]
Re:532 [in MetaCoq.PCUIC.PCUICEquality]
Re:535 [in MetaCoq.PCUIC.PCUICNormal]
Re:535 [in MetaCoq.PCUIC.PCUICConfluence]
Re:540 [in MetaCoq.PCUIC.PCUICEquality]
Re:544 [in MetaCoq.PCUIC.PCUICConfluence]
Re:55 [in MetaCoq.PCUIC.PCUICSN]
Re:552 [in MetaCoq.PCUIC.PCUICEquality]
Re:553 [in MetaCoq.PCUIC.PCUICConfluence]
Re:555 [in MetaCoq.PCUIC.PCUICEquality]
Re:56 [in MetaCoq.PCUIC.PCUICPrincipality]
Re:568 [in MetaCoq.PCUIC.PCUICEquality]
Re:58 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
Re:581 [in MetaCoq.PCUIC.PCUICEquality]
Re:586 [in MetaCoq.PCUIC.PCUICEquality]
Re:589 [in MetaCoq.PCUIC.PCUICEquality]
Re:592 [in MetaCoq.PCUIC.PCUICEquality]
Re:595 [in MetaCoq.PCUIC.PCUICEquality]
Re:602 [in MetaCoq.PCUIC.PCUICEquality]
Re:605 [in MetaCoq.SafeChecker.PCUICSafeChecker]
Re:609 [in MetaCoq.PCUIC.PCUICEquality]
Re:612 [in MetaCoq.PCUIC.PCUICEquality]
Re:617 [in MetaCoq.PCUIC.PCUICEquality]
Re:630 [in MetaCoq.PCUIC.PCUICEquality]
Re:636 [in MetaCoq.PCUIC.PCUICEquality]
Re:64 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
Re:64 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
Re:641 [in MetaCoq.PCUIC.PCUICEquality]
Re:644 [in MetaCoq.PCUIC.PCUICEquality]
Re:652 [in MetaCoq.PCUIC.PCUICEquality]
Re:652 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
Re:666 [in MetaCoq.PCUIC.PCUICEquality]
Re:668 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
Re:673 [in MetaCoq.PCUIC.PCUICEquality]
Re:674 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
Re:677 [in MetaCoq.PCUIC.PCUICEquality]
Re:681 [in MetaCoq.PCUIC.PCUICEquality]
Re:683 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
Re:685 [in MetaCoq.PCUIC.PCUICEquality]
Re:69 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
Re:691 [in MetaCoq.PCUIC.PCUICEquality]
Re:699 [in MetaCoq.PCUIC.PCUICEquality]
Re:72 [in MetaCoq.Template.TermEquality]
Re:75 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
Re:77 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
Re:79 [in MetaCoq.PCUIC.PCUICCumulProp]
Re:8 [in MetaCoq.PCUIC.PCUICEquality]
Re:84 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
Re:86 [in MetaCoq.PCUIC.PCUICConvCumInversion]
rhoargs:693 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho:1 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho:123 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho:132 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho:151 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho:159 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho:164 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho:171 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho:177 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho:182 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho:193 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho:200 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho:211 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho:217 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho:222 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho:231 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho:243 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho:252 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho:259 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho:637 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rh1:86 [in MetaCoq.Examples.tauto]
rh2:87 [in MetaCoq.Examples.tauto]
rh:102 [in MetaCoq.Examples.tauto]
rh:59 [in MetaCoq.Examples.tauto]
rh:65 [in MetaCoq.Examples.tauto]
rh:84 [in MetaCoq.Examples.tauto]
rh:91 [in MetaCoq.Examples.tauto]
rk':162 [in MetaCoq.PCUIC.PCUICCanonicity]
rk:161 [in MetaCoq.PCUIC.PCUICCanonicity]
Rle':177 [in MetaCoq.Template.TermEquality]
Rle':193 [in MetaCoq.Template.TermEquality]
Rle':212 [in MetaCoq.Template.TermEquality]
Rle':220 [in MetaCoq.Template.TermEquality]
Rle':248 [in MetaCoq.PCUIC.PCUICContextConversion]
Rle':339 [in MetaCoq.PCUIC.PCUICEquality]
Rle':346 [in MetaCoq.PCUIC.PCUICEquality]
Rle':357 [in MetaCoq.PCUIC.PCUICEquality]
Rle':372 [in MetaCoq.PCUIC.PCUICEquality]
Rle':379 [in MetaCoq.PCUIC.PCUICEquality]
Rle':47 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
Rle':55 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
Rle':639 [in MetaCoq.PCUIC.PCUICEquality]
Rle':693 [in MetaCoq.PCUIC.PCUICEquality]
Rle':701 [in MetaCoq.PCUIC.PCUICEquality]
Rle:106 [in MetaCoq.PCUIC.PCUICAlpha]
Rle:11 [in MetaCoq.Template.TermEquality]
Rle:1110 [in MetaCoq.PCUIC.PCUICConversion]
Rle:1116 [in MetaCoq.PCUIC.PCUICConversion]
Rle:117 [in MetaCoq.PCUIC.PCUICEquality]
Rle:121 [in MetaCoq.PCUIC.PCUICConfluence]
Rle:123 [in MetaCoq.SafeChecker.PCUICEqualityDec]
Rle:133 [in MetaCoq.SafeChecker.PCUICEqualityDec]
Rle:141 [in MetaCoq.PCUIC.PCUICConfluence]
Rle:15 [in MetaCoq.PCUIC.PCUICEquality]
Rle:152 [in MetaCoq.Template.TermEquality]
Rle:153 [in MetaCoq.SafeChecker.PCUICEqualityDec]
Rle:162 [in MetaCoq.Template.TermEquality]
Rle:172 [in MetaCoq.SafeChecker.PCUICEqualityDec]
Rle:176 [in MetaCoq.Template.TermEquality]
Rle:179 [in MetaCoq.SafeChecker.PCUICEqualityDec]
Rle:191 [in MetaCoq.SafeChecker.PCUICEqualityDec]
Rle:192 [in MetaCoq.Template.TermEquality]
Rle:20 [in MetaCoq.PCUIC.PCUICAlpha]
Rle:206 [in MetaCoq.SafeChecker.PCUICEqualityDec]
Rle:211 [in MetaCoq.Template.TermEquality]
Rle:219 [in MetaCoq.Template.TermEquality]
Rle:219 [in MetaCoq.PCUIC.PCUICEquality]
Rle:226 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
Rle:230 [in MetaCoq.SafeChecker.PCUICEqualityDec]
Rle:231 [in MetaCoq.Template.TermEquality]
Rle:239 [in MetaCoq.PCUIC.PCUICAlpha]
Rle:241 [in MetaCoq.PCUIC.PCUICEquality]
Rle:243 [in MetaCoq.Template.TermEquality]
Rle:246 [in MetaCoq.PCUIC.PCUICContextConversion]
Rle:249 [in MetaCoq.PCUIC.PCUICEquality]
Rle:252 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
Rle:256 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
Rle:260 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
Rle:262 [in MetaCoq.PCUIC.PCUICEquality]
Rle:270 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
Rle:271 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
Rle:271 [in MetaCoq.PCUIC.PCUICEquality]
Rle:275 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
Rle:278 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
Rle:278 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
Rle:28 [in MetaCoq.PCUIC.PCUICEquality]
Rle:281 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
Rle:283 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
Rle:286 [in MetaCoq.PCUIC.PCUICEquality]
Rle:286 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
Rle:288 [in MetaCoq.PCUIC.PCUICConfluence]
Rle:289 [in MetaCoq.PCUIC.PCUICCumulProp]
Rle:294 [in MetaCoq.PCUIC.PCUICConfluence]
Rle:295 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
Rle:297 [in MetaCoq.PCUIC.PCUICConversion]
Rle:3 [in MetaCoq.PCUIC.PCUICCumulativity]
Rle:30 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
Rle:300 [in MetaCoq.PCUIC.PCUICConfluence]
Rle:301 [in MetaCoq.SafeChecker.PCUICEqualityDec]
Rle:302 [in MetaCoq.PCUIC.PCUICConversion]
Rle:308 [in MetaCoq.PCUIC.PCUICConfluence]
Rle:309 [in MetaCoq.SafeChecker.PCUICEqualityDec]
Rle:31 [in MetaCoq.Template.TermEquality]
Rle:310 [in MetaCoq.PCUIC.PCUICEquality]
Rle:318 [in MetaCoq.PCUIC.PCUICConfluence]
Rle:319 [in MetaCoq.PCUIC.PCUICEquality]
Rle:325 [in MetaCoq.PCUIC.PCUICEquality]
Rle:328 [in MetaCoq.PCUIC.PCUICConfluence]
Rle:328 [in MetaCoq.PCUIC.PCUICContextConversion]
Rle:33 [in MetaCoq.PCUIC.PCUICEquality]
Rle:336 [in MetaCoq.PCUIC.PCUICConfluence]
Rle:338 [in MetaCoq.PCUIC.PCUICEquality]
Rle:342 [in MetaCoq.PCUIC.PCUICConfluence]
Rle:345 [in MetaCoq.PCUIC.PCUICEquality]
Rle:350 [in MetaCoq.PCUIC.PCUICConfluence]
Rle:356 [in MetaCoq.PCUIC.PCUICEquality]
Rle:36 [in MetaCoq.Template.TermEquality]
Rle:371 [in MetaCoq.PCUIC.PCUICEquality]
Rle:375 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
Rle:378 [in MetaCoq.PCUIC.PCUICEquality]
Rle:384 [in MetaCoq.PCUIC.PCUICEquality]
Rle:385 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
Rle:389 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
Rle:39 [in MetaCoq.PCUIC.PCUICAlpha]
Rle:392 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
Rle:393 [in MetaCoq.PCUIC.PCUICEquality]
Rle:394 [in MetaCoq.PCUIC.PCUICConfluence]
Rle:397 [in MetaCoq.PCUIC.PCUICEquality]
Rle:40 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
Rle:403 [in MetaCoq.PCUIC.PCUICEquality]
Rle:415 [in MetaCoq.PCUIC.PCUICConfluence]
Rle:43 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
Rle:445 [in MetaCoq.PCUIC.PCUICEquality]
Rle:450 [in MetaCoq.PCUIC.PCUICEquality]
Rle:457 [in MetaCoq.PCUIC.PCUICEquality]
Rle:46 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
Rle:466 [in MetaCoq.PCUIC.PCUICEquality]
Rle:466 [in MetaCoq.PCUIC.PCUICConfluence]
Rle:48 [in MetaCoq.PCUIC.PCUICSN]
Rle:486 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
Rle:487 [in MetaCoq.PCUIC.PCUICConfluence]
Rle:488 [in MetaCoq.PCUIC.PCUICEquality]
Rle:49 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
Rle:494 [in MetaCoq.PCUIC.PCUICEquality]
Rle:5 [in MetaCoq.Template.TermEquality]
Rle:500 [in MetaCoq.PCUIC.PCUICEquality]
Rle:508 [in MetaCoq.PCUIC.PCUICEquality]
Rle:517 [in MetaCoq.PCUIC.PCUICEquality]
Rle:524 [in MetaCoq.PCUIC.PCUICConfluence]
Rle:526 [in MetaCoq.PCUIC.PCUICEquality]
Rle:528 [in MetaCoq.PCUIC.PCUICNormal]
Rle:533 [in MetaCoq.PCUIC.PCUICEquality]
Rle:536 [in MetaCoq.PCUIC.PCUICNormal]
Rle:536 [in MetaCoq.PCUIC.PCUICConfluence]
Rle:54 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
Rle:541 [in MetaCoq.PCUIC.PCUICEquality]
Rle:545 [in MetaCoq.PCUIC.PCUICConfluence]
Rle:553 [in MetaCoq.PCUIC.PCUICEquality]
Rle:554 [in MetaCoq.PCUIC.PCUICConfluence]
Rle:556 [in MetaCoq.PCUIC.PCUICEquality]
Rle:569 [in MetaCoq.PCUIC.PCUICEquality]
Rle:57 [in MetaCoq.PCUIC.PCUICPrincipality]
Rle:582 [in MetaCoq.PCUIC.PCUICEquality]
Rle:587 [in MetaCoq.PCUIC.PCUICEquality]
Rle:590 [in MetaCoq.PCUIC.PCUICEquality]
Rle:593 [in MetaCoq.PCUIC.PCUICEquality]
Rle:596 [in MetaCoq.PCUIC.PCUICEquality]
Rle:603 [in MetaCoq.PCUIC.PCUICEquality]
Rle:606 [in MetaCoq.SafeChecker.PCUICSafeChecker]
Rle:610 [in MetaCoq.PCUIC.PCUICEquality]
Rle:613 [in MetaCoq.PCUIC.PCUICEquality]
Rle:618 [in MetaCoq.PCUIC.PCUICEquality]
Rle:63 [in MetaCoq.SafeChecker.PCUICEqualityDec]
Rle:631 [in MetaCoq.PCUIC.PCUICEquality]
Rle:638 [in MetaCoq.PCUIC.PCUICEquality]
Rle:642 [in MetaCoq.PCUIC.PCUICEquality]
Rle:645 [in MetaCoq.PCUIC.PCUICEquality]
Rle:65 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
Rle:653 [in MetaCoq.PCUIC.PCUICEquality]
Rle:653 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
Rle:667 [in MetaCoq.PCUIC.PCUICEquality]
Rle:669 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
Rle:675 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
Rle:684 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
Rle:688 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
Rle:691 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
Rle:692 [in MetaCoq.PCUIC.PCUICEquality]
Rle:70 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
Rle:70 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
Rle:70 [in MetaCoq.SafeChecker.PCUICEqualityDec]
Rle:700 [in MetaCoq.PCUIC.PCUICEquality]
Rle:73 [in MetaCoq.Template.TermEquality]
Rle:73 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
Rle:76 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
Rle:78 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
Rle:80 [in MetaCoq.PCUIC.PCUICCumulProp]
Rle:85 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
Rle:87 [in MetaCoq.PCUIC.PCUICConvCumInversion]
Rle:9 [in MetaCoq.PCUIC.PCUICEquality]
rs:2866 [in MetaCoq.Translations.MiniHoTT]
rs:2874 [in MetaCoq.Translations.MiniHoTT_paths]
Ru:238 [in MetaCoq.PCUIC.PCUICEquality]
Ru:265 [in MetaCoq.PCUIC.PCUICEquality]
Ru:283 [in MetaCoq.PCUIC.PCUICEquality]
rx:2536 [in MetaCoq.Template.utils.All_Forall]
R':1270 [in MetaCoq.Template.utils.All_Forall]
r':1297 [in MetaCoq.Translations.MiniHoTT]
r':1305 [in MetaCoq.Translations.MiniHoTT_paths]
R':131 [in MetaCoq.SafeChecker.PCUICSafeReduce]
r':1427 [in MetaCoq.Template.utils.All_Forall]
r':16 [in MetaCoq.Template.Reflect]
R':1629 [in MetaCoq.Template.utils.All_Forall]
r':2061 [in MetaCoq.Template.utils.All_Forall]
R':2362 [in MetaCoq.SafeChecker.PCUICSafeConversion]
R':33 [in MetaCoq.PCUIC.PCUICSN]
R':40 [in MetaCoq.Template.TermEquality]
R':42 [in MetaCoq.Template.TermEquality]
R':43 [in MetaCoq.PCUIC.PCUICEquality]
R':45 [in MetaCoq.PCUIC.PCUICEquality]
r':54 [in MetaCoq.Template.Reflect]
r':758 [in MetaCoq.Template.utils.MCList]
r':763 [in MetaCoq.Template.utils.MCList]
R1:1022 [in MetaCoq.Template.utils.All_Forall]
R1:1037 [in MetaCoq.Template.utils.All_Forall]
r1:1336 [in MetaCoq.Translations.MiniHoTT]
r1:1344 [in MetaCoq.Translations.MiniHoTT_paths]
r1:1464 [in MetaCoq.Template.utils.All_Forall]
r1:1470 [in MetaCoq.Template.utils.All_Forall]
r1:1479 [in MetaCoq.Template.utils.All_Forall]
r1:1952 [in MetaCoq.Template.utils.All_Forall]
R1:225 [in MetaCoq.PCUIC.PCUICSR]
R1:238 [in MetaCoq.PCUIC.PCUICSR]
R1:338 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
R1:427 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
R1:648 [in MetaCoq.Template.utils.All_Forall]
R1:660 [in MetaCoq.Template.utils.All_Forall]
R1:708 [in MetaCoq.Template.utils.All_Forall]
R1:719 [in MetaCoq.Template.utils.All_Forall]
R1:826 [in MetaCoq.Template.utils.All_Forall]
R1:840 [in MetaCoq.Template.utils.All_Forall]
r1:868 [in MetaCoq.Translations.MiniHoTT]
r1:876 [in MetaCoq.Translations.MiniHoTT_paths]
R2:1023 [in MetaCoq.Template.utils.All_Forall]
R2:1038 [in MetaCoq.Template.utils.All_Forall]
r2:1337 [in MetaCoq.Translations.MiniHoTT]
r2:1345 [in MetaCoq.Translations.MiniHoTT_paths]
r2:1465 [in MetaCoq.Template.utils.All_Forall]
r2:1471 [in MetaCoq.Template.utils.All_Forall]
r2:1480 [in MetaCoq.Template.utils.All_Forall]
r2:1953 [in MetaCoq.Template.utils.All_Forall]
R2:226 [in MetaCoq.PCUIC.PCUICSR]
R2:239 [in MetaCoq.PCUIC.PCUICSR]
R2:339 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
R2:428 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
R2:649 [in MetaCoq.Template.utils.All_Forall]
R2:661 [in MetaCoq.Template.utils.All_Forall]
R2:709 [in MetaCoq.Template.utils.All_Forall]
R2:720 [in MetaCoq.Template.utils.All_Forall]
R2:827 [in MetaCoq.Template.utils.All_Forall]
R2:841 [in MetaCoq.Template.utils.All_Forall]
r2:869 [in MetaCoq.Translations.MiniHoTT]
r2:877 [in MetaCoq.Translations.MiniHoTT_paths]
R3:1024 [in MetaCoq.Template.utils.All_Forall]
R3:1039 [in MetaCoq.Template.utils.All_Forall]
R3:227 [in MetaCoq.PCUIC.PCUICSR]
R3:240 [in MetaCoq.PCUIC.PCUICSR]
R3:341 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
R3:430 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
R3:650 [in MetaCoq.Template.utils.All_Forall]
R3:662 [in MetaCoq.Template.utils.All_Forall]
R3:710 [in MetaCoq.Template.utils.All_Forall]
R3:721 [in MetaCoq.Template.utils.All_Forall]
R3:828 [in MetaCoq.Template.utils.All_Forall]
R3:842 [in MetaCoq.Template.utils.All_Forall]
R:1 [in MetaCoq.Template.TermEquality]
r:1 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
r:1003 [in MetaCoq.Template.utils.All_Forall]
R:1007 [in MetaCoq.PCUIC.PCUICConfluence]
R:103 [in MetaCoq.Template.utils.MCRelations]
R:1051 [in MetaCoq.PCUIC.PCUICConfluence]
r:106 [in MetaCoq.PCUIC.PCUICConfluence]
R:107 [in MetaCoq.Template.monad_utils]
R:1075 [in MetaCoq.PCUIC.PCUICConfluence]
r:1081 [in MetaCoq.Translations.MiniHoTT]
r:1087 [in MetaCoq.Translations.MiniHoTT]
r:1089 [in MetaCoq.Translations.MiniHoTT_paths]
r:1094 [in MetaCoq.Translations.MiniHoTT]
r:1095 [in MetaCoq.Translations.MiniHoTT_paths]
r:1102 [in MetaCoq.Translations.MiniHoTT_paths]
r:1103 [in MetaCoq.Translations.MiniHoTT]
r:1110 [in MetaCoq.Translations.MiniHoTT]
r:1111 [in MetaCoq.Translations.MiniHoTT_paths]
r:1118 [in MetaCoq.Translations.MiniHoTT]
r:1118 [in MetaCoq.Translations.MiniHoTT_paths]
R:112 [in MetaCoq.Template.utils.All_Forall]
r:1126 [in MetaCoq.Translations.MiniHoTT_paths]
r:1146 [in MetaCoq.PCUIC.PCUICConfluence]
R:116 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
R:119 [in MetaCoq.Template.utils.All_Forall]
R:119 [in MetaCoq.SafeChecker.PCUICSafeReduce]
r:1192 [in MetaCoq.Translations.MiniHoTT]
r:1200 [in MetaCoq.Translations.MiniHoTT_paths]
r:1202 [in MetaCoq.Translations.MiniHoTT]
r:1210 [in MetaCoq.Translations.MiniHoTT_paths]
r:1211 [in MetaCoq.Translations.MiniHoTT]
R:1217 [in MetaCoq.PCUIC.PCUICConfluence]
r:1219 [in MetaCoq.Translations.MiniHoTT]
r:1219 [in MetaCoq.Translations.MiniHoTT_paths]
r:1226 [in MetaCoq.Translations.MiniHoTT]
r:1227 [in MetaCoq.Translations.MiniHoTT_paths]
r:1234 [in MetaCoq.Translations.MiniHoTT]
r:1234 [in MetaCoq.Translations.MiniHoTT_paths]
r:1242 [in MetaCoq.Translations.MiniHoTT_paths]
r:1268 [in MetaCoq.Translations.MiniHoTT]
R:1269 [in MetaCoq.Template.utils.All_Forall]
r:1276 [in MetaCoq.Translations.MiniHoTT_paths]
r:1287 [in MetaCoq.Translations.MiniHoTT]
r:129 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
r:1295 [in MetaCoq.Translations.MiniHoTT_paths]
r:1296 [in MetaCoq.Translations.MiniHoTT]
r:13 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
R:130 [in MetaCoq.SafeChecker.PCUICSafeReduce]
r:1304 [in MetaCoq.Translations.MiniHoTT_paths]
r:1308 [in MetaCoq.Translations.MiniHoTT]
r:1316 [in MetaCoq.Translations.MiniHoTT_paths]
r:1318 [in MetaCoq.Translations.MiniHoTT]
r:1326 [in MetaCoq.Translations.MiniHoTT]
r:1326 [in MetaCoq.Translations.MiniHoTT_paths]
R:133 [in MetaCoq.PCUIC.PCUICSafeLemmata]
r:1334 [in MetaCoq.Translations.MiniHoTT_paths]
R:1337 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
r:1342 [in MetaCoq.Translations.MiniHoTT]
r:135 [in MetaCoq.Translations.MiniHoTT]
r:1350 [in MetaCoq.Translations.MiniHoTT]
r:1350 [in MetaCoq.Translations.MiniHoTT_paths]
r:1358 [in MetaCoq.Translations.MiniHoTT_paths]
r:136 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
r:1366 [in MetaCoq.Translations.MiniHoTT]
r:1367 [in MetaCoq.Translations.MiniHoTT]
R:1370 [in MetaCoq.SafeChecker.PCUICSafeReduce]
r:1374 [in MetaCoq.Translations.MiniHoTT_paths]
r:1375 [in MetaCoq.Translations.MiniHoTT_paths]
R:139 [in MetaCoq.PCUIC.PCUICSafeLemmata]
R:14 [in MetaCoq.PCUIC.PCUICConfluence]
r:142 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
r:1426 [in MetaCoq.Template.utils.All_Forall]
r:143 [in MetaCoq.Translations.MiniHoTT_paths]
R:1432 [in MetaCoq.Template.utils.All_Forall]
r:145 [in MetaCoq.Template.Typing]
R:146 [in MetaCoq.PCUIC.utils.PCUICUtils]
R:1460 [in MetaCoq.Template.utils.All_Forall]
r:1463 [in MetaCoq.Template.utils.All_Forall]
R:1468 [in MetaCoq.Template.utils.All_Forall]
R:1483 [in MetaCoq.Template.utils.All_Forall]
r:149 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
r:1491 [in MetaCoq.Template.utils.All_Forall]
R:1498 [in MetaCoq.Template.utils.All_Forall]
R:15 [in MetaCoq.Template.utils.MCReflect]
R:15 [in MetaCoq.Template.utils.MCRelations]
r:15 [in MetaCoq.Template.Reflect]
r:150 [in MetaCoq.Template.Typing]
r:1506 [in MetaCoq.Template.utils.All_Forall]
R:1513 [in MetaCoq.Template.utils.All_Forall]
r:155 [in MetaCoq.Template.Typing]
R:1584 [in MetaCoq.Template.utils.All_Forall]
R:1588 [in MetaCoq.Template.utils.All_Forall]
R:1592 [in MetaCoq.Template.utils.All_Forall]
r:16 [in MetaCoq.Template.utils.MCReflect]
R:16 [in MetaCoq.Template.utils.All_Forall]
r:16 [in MetaCoq.PCUIC.PCUICTyping]
R:160 [in MetaCoq.SafeChecker.PCUICEqualityDec]
R:1601 [in MetaCoq.Template.utils.All_Forall]
R:1610 [in MetaCoq.Template.utils.All_Forall]
R:1628 [in MetaCoq.Template.utils.All_Forall]
R:1636 [in MetaCoq.Template.utils.All_Forall]
R:1644 [in MetaCoq.Template.utils.All_Forall]
R:1684 [in MetaCoq.Template.utils.All_Forall]
R:1691 [in MetaCoq.Template.utils.All_Forall]
R:1706 [in MetaCoq.Template.utils.All_Forall]
R:172 [in MetaCoq.PCUIC.PCUICContextConversion]
R:1726 [in MetaCoq.Template.utils.All_Forall]
R:1736 [in MetaCoq.Template.utils.All_Forall]
R:1776 [in MetaCoq.Template.utils.All_Forall]
R:1783 [in MetaCoq.Template.utils.All_Forall]
r:18 [in MetaCoq.PCUIC.PCUICTyping]
r:18 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
R:1842 [in MetaCoq.Template.utils.All_Forall]
r:1852 [in MetaCoq.Translations.MiniHoTT]
r:1853 [in MetaCoq.Translations.MiniHoTT]
r:1854 [in MetaCoq.Translations.MiniHoTT]
R:186 [in MetaCoq.PCUIC.PCUICContextConversion]
r:1860 [in MetaCoq.Translations.MiniHoTT_paths]
r:1861 [in MetaCoq.Translations.MiniHoTT_paths]
r:1862 [in MetaCoq.Translations.MiniHoTT]
r:1862 [in MetaCoq.Translations.MiniHoTT_paths]
r:1869 [in MetaCoq.Translations.MiniHoTT]
r:1870 [in MetaCoq.Translations.MiniHoTT_paths]
r:1876 [in MetaCoq.Translations.MiniHoTT]
r:1877 [in MetaCoq.Translations.MiniHoTT_paths]
r:1883 [in MetaCoq.Translations.MiniHoTT]
r:1884 [in MetaCoq.Translations.MiniHoTT_paths]
r:1890 [in MetaCoq.Translations.MiniHoTT]
r:1891 [in MetaCoq.Translations.MiniHoTT_paths]
r:1897 [in MetaCoq.Translations.MiniHoTT]
r:1898 [in MetaCoq.Translations.MiniHoTT_paths]
r:1905 [in MetaCoq.Translations.MiniHoTT]
r:1905 [in MetaCoq.Translations.MiniHoTT_paths]
r:1913 [in MetaCoq.Translations.MiniHoTT]
r:1913 [in MetaCoq.Translations.MiniHoTT_paths]
r:1920 [in MetaCoq.Translations.MiniHoTT]
r:1921 [in MetaCoq.Translations.MiniHoTT_paths]
r:1927 [in MetaCoq.Translations.MiniHoTT]
r:1928 [in MetaCoq.Translations.MiniHoTT_paths]
r:1934 [in MetaCoq.Translations.MiniHoTT]
r:1935 [in MetaCoq.Translations.MiniHoTT_paths]
R:1938 [in MetaCoq.Template.utils.All_Forall]
r:1941 [in MetaCoq.Translations.MiniHoTT]
r:1942 [in MetaCoq.Translations.MiniHoTT_paths]
R:1948 [in MetaCoq.Template.utils.All_Forall]
r:1948 [in MetaCoq.Translations.MiniHoTT]
r:1949 [in MetaCoq.Translations.MiniHoTT_paths]
r:1955 [in MetaCoq.Translations.MiniHoTT]
r:1956 [in MetaCoq.Translations.MiniHoTT_paths]
R:1958 [in MetaCoq.Template.utils.All_Forall]
r:1962 [in MetaCoq.Translations.MiniHoTT]
r:1963 [in MetaCoq.Translations.MiniHoTT_paths]
R:1969 [in MetaCoq.Template.utils.All_Forall]
r:1969 [in MetaCoq.Translations.MiniHoTT]
r:1970 [in MetaCoq.Translations.MiniHoTT_paths]
r:1976 [in MetaCoq.Translations.MiniHoTT]
r:1977 [in MetaCoq.Translations.MiniHoTT_paths]
R:1979 [in MetaCoq.Template.utils.All_Forall]
r:198 [in MetaCoq.PCUIC.PCUICInductiveInversion]
r:1983 [in MetaCoq.Translations.MiniHoTT]
r:1984 [in MetaCoq.Translations.MiniHoTT_paths]
R:1988 [in MetaCoq.Template.utils.All_Forall]
r:1990 [in MetaCoq.Translations.MiniHoTT]
r:1991 [in MetaCoq.Translations.MiniHoTT_paths]
r:1997 [in MetaCoq.Translations.MiniHoTT]
r:1998 [in MetaCoq.Translations.MiniHoTT_paths]
R:2 [in MetaCoq.PCUIC.utils.PCUICOnOne]
R:2 [in MetaCoq.SafeChecker.PCUICWfReduction]
R:20 [in MetaCoq.Template.utils.MCReflect]
r:200 [in MetaCoq.Translations.MiniHoTT]
r:2004 [in MetaCoq.Translations.MiniHoTT]
r:2005 [in MetaCoq.Translations.MiniHoTT_paths]
r:2011 [in MetaCoq.Translations.MiniHoTT]
r:2012 [in MetaCoq.Translations.MiniHoTT_paths]
r:2018 [in MetaCoq.Translations.MiniHoTT]
r:2019 [in MetaCoq.Translations.MiniHoTT_paths]
R:2025 [in MetaCoq.Template.utils.All_Forall]
r:2025 [in MetaCoq.Translations.MiniHoTT]
r:2026 [in MetaCoq.Translations.MiniHoTT_paths]
R:2031 [in MetaCoq.Template.utils.All_Forall]
r:2032 [in MetaCoq.Translations.MiniHoTT]
r:2033 [in MetaCoq.Translations.MiniHoTT_paths]
R:2038 [in MetaCoq.Template.utils.All_Forall]
r:2040 [in MetaCoq.Translations.MiniHoTT_paths]
R:2047 [in MetaCoq.Template.utils.All_Forall]
R:2053 [in MetaCoq.Template.utils.All_Forall]
r:2060 [in MetaCoq.Template.utils.All_Forall]
R:2069 [in MetaCoq.Template.utils.All_Forall]
r:208 [in MetaCoq.Translations.MiniHoTT]
r:208 [in MetaCoq.Translations.MiniHoTT_paths]
r:21 [in MetaCoq.Template.utils.MCReflect]
R:213 [in MetaCoq.SafeChecker.PCUICEqualityDec]
R:2135 [in MetaCoq.Template.utils.All_Forall]
R:2147 [in MetaCoq.Template.utils.All_Forall]
R:2157 [in MetaCoq.Template.utils.All_Forall]
R:216 [in MetaCoq.Template.utils.All_Forall]
r:216 [in MetaCoq.Translations.MiniHoTT_paths]
r:216 [in MetaCoq.PCUIC.PCUICContextConversion]
R:2166 [in MetaCoq.Template.utils.All_Forall]
R:2192 [in MetaCoq.Template.utils.All_Forall]
R:22 [in MetaCoq.Template.utils.MCOption]
r:22 [in MetaCoq.PCUIC.PCUICTyping]
R:2201 [in MetaCoq.Template.utils.All_Forall]
R:2210 [in MetaCoq.Template.utils.All_Forall]
R:2216 [in MetaCoq.Template.utils.All_Forall]
R:222 [in MetaCoq.Template.TypingWf]
r:2223 [in MetaCoq.Translations.MiniHoTT]
R:2228 [in MetaCoq.Template.utils.All_Forall]
r:2231 [in MetaCoq.Translations.MiniHoTT]
r:2231 [in MetaCoq.Translations.MiniHoTT_paths]
r:2238 [in MetaCoq.Translations.MiniHoTT]
r:2239 [in MetaCoq.Translations.MiniHoTT_paths]
R:2242 [in MetaCoq.Template.utils.All_Forall]
r:2246 [in MetaCoq.Translations.MiniHoTT_paths]
r:2248 [in MetaCoq.Translations.MiniHoTT]
r:2256 [in MetaCoq.Translations.MiniHoTT_paths]
r:2258 [in MetaCoq.Translations.MiniHoTT]
r:2266 [in MetaCoq.Translations.MiniHoTT_paths]
r:2268 [in MetaCoq.Translations.MiniHoTT]
R:227 [in MetaCoq.Template.utils.All_Forall]
r:2276 [in MetaCoq.Translations.MiniHoTT_paths]
r:2278 [in MetaCoq.Translations.MiniHoTT]
r:228 [in MetaCoq.PCUIC.PCUICReduction]
r:2286 [in MetaCoq.Translations.MiniHoTT_paths]
r:2288 [in MetaCoq.Translations.MiniHoTT]
r:2295 [in MetaCoq.Translations.MiniHoTT]
r:2296 [in MetaCoq.Translations.MiniHoTT_paths]
r:2303 [in MetaCoq.Translations.MiniHoTT_paths]
r:234 [in MetaCoq.PCUIC.PCUICReduction]
R:236 [in MetaCoq.SafeChecker.PCUICEqualityDec]
R:2361 [in MetaCoq.SafeChecker.PCUICSafeConversion]
R:238 [in MetaCoq.Template.utils.All_Forall]
R:239 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
r:24 [in MetaCoq.Template.BasicAst]
R:24 [in MetaCoq.Template.utils.MCRelations]
r:240 [in MetaCoq.PCUIC.PCUICReduction]
R:2493 [in MetaCoq.Translations.MiniHoTT]
R:25 [in MetaCoq.Template.utils.All_Forall]
R:25 [in MetaCoq.Translations.MiniHoTT]
R:2501 [in MetaCoq.Translations.MiniHoTT_paths]
R:2528 [in MetaCoq.Template.utils.All_Forall]
R:2569 [in MetaCoq.Template.utils.All_Forall]
R:2584 [in MetaCoq.Translations.MiniHoTT]
R:2592 [in MetaCoq.Translations.MiniHoTT_paths]
R:26 [in MetaCoq.Template.utils.MCRelations]
R:263 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
r:275 [in MetaCoq.Translations.MiniHoTT]
r:2771 [in MetaCoq.Translations.MiniHoTT]
r:2772 [in MetaCoq.Translations.MiniHoTT]
r:2779 [in MetaCoq.Translations.MiniHoTT_paths]
r:2780 [in MetaCoq.Translations.MiniHoTT_paths]
r:28 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
r:282 [in MetaCoq.Translations.MiniHoTT]
r:283 [in MetaCoq.Translations.MiniHoTT_paths]
r:2864 [in MetaCoq.Translations.MiniHoTT]
r:2872 [in MetaCoq.Translations.MiniHoTT_paths]
r:2873 [in MetaCoq.Translations.MiniHoTT]
r:2881 [in MetaCoq.Translations.MiniHoTT_paths]
r:289 [in MetaCoq.Translations.MiniHoTT]
r:290 [in MetaCoq.Translations.MiniHoTT_paths]
r:296 [in MetaCoq.Translations.MiniHoTT]
r:297 [in MetaCoq.Translations.MiniHoTT_paths]
R:3 [in MetaCoq.Template.utils.MCRelations]
R:30 [in MetaCoq.PCUIC.PCUICConfluence]
R:30 [in MetaCoq.Translations.MiniHoTT]
r:303 [in MetaCoq.Translations.MiniHoTT]
r:304 [in MetaCoq.Translations.MiniHoTT_paths]
R:307 [in MetaCoq.PCUIC.PCUICEquality]
r:31 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
r:310 [in MetaCoq.Translations.MiniHoTT]
r:311 [in MetaCoq.Translations.MiniHoTT_paths]
R:313 [in MetaCoq.PCUIC.PCUICEquality]
r:317 [in MetaCoq.Translations.MiniHoTT]
r:318 [in MetaCoq.Translations.MiniHoTT_paths]
r:319 [in MetaCoq.Template.Typing]
r:32 [in MetaCoq.Template.utils.All_Forall]
R:32 [in MetaCoq.PCUIC.PCUICSN]
r:324 [in MetaCoq.Translations.MiniHoTT]
r:325 [in MetaCoq.Template.Typing]
r:325 [in MetaCoq.Translations.MiniHoTT_paths]
R:325 [in MetaCoq.SafeChecker.PCUICEqualityDec]
R:33 [in MetaCoq.Template.utils.MCRelations]
R:33 [in MetaCoq.Translations.MiniHoTT_paths]
r:331 [in MetaCoq.Template.Typing]
r:332 [in MetaCoq.Translations.MiniHoTT_paths]
r:35 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
R:351 [in MetaCoq.SafeChecker.PCUICEqualityDec]
r:36 [in MetaCoq.Translations.times_bool_fun]
R:36 [in MetaCoq.Template.utils.All_Forall]
R:36 [in MetaCoq.Translations.MiniHoTT]
r:366 [in MetaCoq.PCUIC.PCUICReduction]
R:369 [in MetaCoq.Template.utils.All_Forall]
R:37 [in MetaCoq.Template.utils.MCRelations]
r:37 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
R:371 [in MetaCoq.Template.utils.All_Forall]
R:38 [in MetaCoq.Translations.MiniHoTT_paths]
R:39 [in MetaCoq.Template.TermEquality]
r:398 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
R:40 [in MetaCoq.Template.utils.MCRelations]
R:40 [in MetaCoq.Template.utils.ReflectEq]
r:401 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
r:404 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
r:408 [in MetaCoq.PCUIC.PCUICSR]
R:41 [in MetaCoq.Template.TermEquality]
r:414 [in MetaCoq.PCUIC.PCUICSR]
R:42 [in MetaCoq.PCUIC.PCUICEquality]
r:420 [in MetaCoq.PCUIC.PCUICSR]
r:43 [in MetaCoq.Translations.times_bool_fun]
R:43 [in MetaCoq.Template.utils.MCRelations]
R:43 [in MetaCoq.Template.utils.ReflectEq]
R:43 [in MetaCoq.Translations.MiniHoTT]
R:44 [in MetaCoq.PCUIC.PCUICEquality]
R:44 [in MetaCoq.Translations.MiniHoTT_paths]
r:449 [in MetaCoq.Translations.MiniHoTT]
r:457 [in MetaCoq.Translations.MiniHoTT_paths]
R:46 [in MetaCoq.Template.utils.MCRelations]
R:46 [in MetaCoq.Erasure.ErasureFunction]
r:461 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
r:461 [in MetaCoq.Translations.MiniHoTT]
r:469 [in MetaCoq.Translations.MiniHoTT_paths]
R:47 [in MetaCoq.Template.utils.ReflectEq]
R:47 [in MetaCoq.SafeChecker.PCUICSafeReduce]
R:49 [in MetaCoq.Template.utils.MCRelations]
R:5 [in MetaCoq.PCUIC.PCUICEquality]
r:5 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
R:51 [in MetaCoq.Template.utils.MCRelations]
R:51 [in MetaCoq.Translations.MiniHoTT_paths]
R:516 [in MetaCoq.PCUIC.PCUICConfluence]
R:519 [in MetaCoq.PCUIC.PCUICConfluence]
R:526 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
r:53 [in MetaCoq.Template.Reflect]
r:53 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
r:535 [in MetaCoq.Translations.MiniHoTT]
R:54 [in MetaCoq.Template.utils.MCRelations]
r:543 [in MetaCoq.Translations.MiniHoTT_paths]
r:546 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
r:547 [in MetaCoq.Translations.MiniHoTT]
R:554 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
r:555 [in MetaCoq.Translations.MiniHoTT_paths]
r:557 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
r:568 [in MetaCoq.Translations.MiniHoTT]
R:569 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
R:575 [in MetaCoq.PCUIC.PCUICEquality]
r:576 [in MetaCoq.Translations.MiniHoTT_paths]
r:577 [in MetaCoq.Template.Typing]
R:577 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
r:579 [in MetaCoq.Template.Typing]
r:579 [in MetaCoq.Translations.MiniHoTT]
R:582 [in MetaCoq.PCUIC.PCUICConversion]
r:583 [in MetaCoq.Template.Typing]
r:587 [in MetaCoq.Translations.MiniHoTT_paths]
r:589 [in MetaCoq.Translations.MiniHoTT]
r:597 [in MetaCoq.Translations.MiniHoTT_paths]
r:6 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
r:60 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
r:607 [in MetaCoq.Translations.MiniHoTT]
r:615 [in MetaCoq.Translations.MiniHoTT_paths]
r:62 [in MetaCoq.PCUIC.PCUICReduction]
r:624 [in MetaCoq.Template.utils.All_Forall]
R:624 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
R:626 [in MetaCoq.Template.utils.All_Forall]
R:630 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
r:635 [in MetaCoq.Template.utils.All_Forall]
R:64 [in MetaCoq.Template.utils.MCRelations]
R:661 [in MetaCoq.PCUIC.PCUICParallelReduction]
r:67 [in MetaCoq.PCUIC.PCUICReduction]
R:72 [in MetaCoq.Template.utils.MCRelations]
r:72 [in MetaCoq.PCUIC.PCUICReduction]
r:727 [in MetaCoq.Translations.MiniHoTT]
r:73 [in MetaCoq.Template.utils.bytestring]
R:732 [in MetaCoq.PCUIC.PCUICParallelReduction]
r:734 [in MetaCoq.Translations.MiniHoTT]
r:735 [in MetaCoq.Translations.MiniHoTT_paths]
r:742 [in MetaCoq.Translations.MiniHoTT_paths]
r:743 [in MetaCoq.Translations.MiniHoTT]
R:75 [in MetaCoq.Template.utils.MCRelations]
r:751 [in MetaCoq.Translations.MiniHoTT_paths]
r:757 [in MetaCoq.Template.utils.MCList]
R:76 [in MetaCoq.PCUIC.utils.PCUICOnOne]
R:76 [in MetaCoq.Translations.times_bool_fun2]
r:762 [in MetaCoq.Template.utils.MCList]
R:764 [in MetaCoq.PCUIC.PCUICReduction]
R:774 [in MetaCoq.PCUIC.PCUICConfluence]
R:778 [in MetaCoq.PCUIC.PCUICConfluence]
R:78 [in MetaCoq.Template.utils.MCRelations]
R:782 [in MetaCoq.PCUIC.PCUICConfluence]
R:788 [in MetaCoq.PCUIC.PCUICConfluence]
R:791 [in MetaCoq.PCUIC.PCUICConfluence]
r:797 [in MetaCoq.Template.utils.All_Forall]
R:799 [in MetaCoq.Template.utils.All_Forall]
r:8 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
R:8 [in MetaCoq.SafeChecker.PCUICSafeChecker]
R:81 [in MetaCoq.Template.utils.MCRelations]
r:810 [in MetaCoq.Template.utils.All_Forall]
R:810 [in MetaCoq.PCUIC.PCUICConfluence]
r:811 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
R:813 [in MetaCoq.PCUIC.PCUICConfluence]
R:82 [in MetaCoq.PCUIC.utils.PCUICOnOne]
r:820 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
r:826 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
r:834 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
r:838 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
R:84 [in MetaCoq.Template.utils.MCRelations]
R:84 [in MetaCoq.SafeChecker.PCUICEqualityDec]
r:843 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
r:85 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
r:850 [in MetaCoq.Translations.MiniHoTT]
r:850 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
r:854 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
r:858 [in MetaCoq.Translations.MiniHoTT_paths]
r:859 [in MetaCoq.Translations.MiniHoTT]
r:867 [in MetaCoq.Translations.MiniHoTT_paths]
R:87 [in MetaCoq.Template.utils.MCRelations]
r:87 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
r:877 [in MetaCoq.Translations.MiniHoTT]
R:88 [in MetaCoq.PCUIC.utils.PCUICOnOne]
r:885 [in MetaCoq.Translations.MiniHoTT_paths]
r:887 [in MetaCoq.Translations.MiniHoTT]
R:89 [in MetaCoq.Template.utils.MCRelations]
r:890 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
r:893 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
r:895 [in MetaCoq.Translations.MiniHoTT_paths]
r:898 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
R:9 [in MetaCoq.Template.utils.MCRelations]
R:90 [in MetaCoq.PCUIC.PCUICConfluence]
r:906 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
R:91 [in MetaCoq.Template.utils.MCRelations]
R:91 [in MetaCoq.SafeChecker.PCUICEqualityDec]
r:913 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
r:917 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
r:920 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
R:920 [in MetaCoq.PCUIC.PCUICReduction]
R:926 [in MetaCoq.PCUIC.PCUICReduction]
r:928 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
R:93 [in MetaCoq.Template.utils.MCRelations]
R:93 [in MetaCoq.PCUIC.utils.PCUICOnOne]
R:934 [in MetaCoq.PCUIC.PCUICConfluence]
r:936 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
R:942 [in MetaCoq.PCUIC.PCUICConfluence]
r:945 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
R:945 [in MetaCoq.PCUIC.PCUICReduction]
R:949 [in MetaCoq.PCUIC.PCUICParallelReduction]
R:95 [in MetaCoq.Template.utils.MCRelations]
R:950 [in MetaCoq.PCUIC.PCUICConfluence]
R:951 [in MetaCoq.PCUIC.PCUICConfluence]
r:951 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
r:955 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
r:96 [in MetaCoq.PCUIC.PCUICConfluence]
R:964 [in MetaCoq.PCUIC.PCUICConfluence]
r:967 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
R:97 [in MetaCoq.Template.utils.MCRelations]
r:971 [in MetaCoq.Translations.MiniHoTT]
r:972 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
R:975 [in MetaCoq.PCUIC.PCUICConfluence]
R:976 [in MetaCoq.PCUIC.PCUICConfluence]
r:977 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
r:979 [in MetaCoq.Translations.MiniHoTT_paths]
R:98 [in MetaCoq.SafeChecker.PCUICWfEnv]
r:981 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
R:984 [in MetaCoq.PCUIC.PCUICConfluence]
r:984 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
R:985 [in MetaCoq.PCUIC.PCUICConfluence]
R:986 [in MetaCoq.PCUIC.PCUICConfluence]
r:988 [in MetaCoq.Template.utils.All_Forall]
R:988 [in MetaCoq.PCUIC.PCUICConfluence]
R:99 [in MetaCoq.Template.utils.MCRelations]
R:99 [in MetaCoq.PCUIC.PCUICConfluence]
R:990 [in MetaCoq.PCUIC.PCUICConfluence]
R:991 [in MetaCoq.Template.utils.All_Forall]
R:992 [in MetaCoq.PCUIC.PCUICConfluence]
rΓ:1139 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rΓ:1150 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rΓ:1361 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rΓ:1368 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
| 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 | (75519 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 | (245 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 | (61331 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 | (144 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (89 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (236 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 | (6913 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 | (1141 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (34 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 | (269 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 | (443 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 | (296 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 | (604 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 | (248 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 | (3386 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (140 entries) |