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 | (69982 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 | (1000 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 | (45451 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 | (770 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 | (1516 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 | (577 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 | (11564 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 | (981 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 | (622 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 | (299 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 | (472 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 | (482 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 | (843 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 | (1156 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 | (4086 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 | (163 entries) |

## J

j [projection, in Coq.Logic.Berardi]JMeq [inductive, in Coq.Logic.JMeq]

JMeq [library]

JMeq_eq_dep [lemma, in Coq.Logic.JMeq]

JMeq_eq_dep_id [lemma, in Coq.Logic.JMeq]

JMeq_congr [lemma, in Coq.Logic.JMeq]

JMeq_rect_r [lemma, in Coq.Logic.JMeq]

JMeq_rec_r [lemma, in Coq.Logic.JMeq]

JMeq_ind_r [lemma, in Coq.Logic.JMeq]

JMeq_rect [lemma, in Coq.Logic.JMeq]

JMeq_rec [lemma, in Coq.Logic.JMeq]

JMeq_ind [lemma, in Coq.Logic.JMeq]

JMeq_eq [axiom, in Coq.Logic.JMeq]

JMeq_trans [lemma, in Coq.Logic.JMeq]

JMeq_sym [lemma, in Coq.Logic.JMeq]

JMeq_hom [definition, in Coq.Logic.JMeq]

JMeq_refl [constructor, in Coq.Logic.JMeq]

JMeq_eq_refl [lemma, in Coq.Program.Equality]

jmp:278 [binder, in Coq.micromega.ZMicromega]

jmp:282 [binder, in Coq.micromega.ZMicromega]

jmp:285 [binder, in Coq.micromega.RingMicromega]

jump [definition, in Coq.setoid_ring.BinList]

jump [definition, in Coq.micromega.Env]

jump_pred_double [lemma, in Coq.setoid_ring.BinList]

jump_add [lemma, in Coq.setoid_ring.BinList]

jump_succ [lemma, in Coq.setoid_ring.BinList]

jump_tl [lemma, in Coq.setoid_ring.BinList]

jump_add' [lemma, in Coq.setoid_ring.Ring_polynom]

jump_pred_double [lemma, in Coq.micromega.Env]

jump_succ [lemma, in Coq.micromega.Env]

jump_tl [lemma, in Coq.micromega.Env]

jump_simpl [lemma, in Coq.micromega.Env]

jump_add [lemma, in Coq.micromega.Env]

j1:313 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]

j1:318 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]

j1:335 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]

j1:341 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]

j1:391 [binder, in Coq.Numbers.Cyclic.Int63.Int63]

j1:396 [binder, in Coq.Numbers.Cyclic.Int63.Int63]

j1:420 [binder, in Coq.Numbers.Cyclic.Int63.Int63]

j1:426 [binder, in Coq.Numbers.Cyclic.Int63.Int63]

j2 [projection, in Coq.Logic.Berardi]

j:10 [binder, in Coq.Reals.Cauchy.ConstructiveRcomplete]

j:10 [binder, in Coq.micromega.Env]

j:100 [binder, in Coq.Reals.Abstract.ConstructiveReals]

j:100 [binder, in Coq.setoid_ring.Ring_polynom]

j:101 [binder, in Coq.Numbers.Cyclic.Int31.Int31]

j:102 [binder, in Coq.micromega.EnvRing]

j:11 [binder, in Coq.setoid_ring.BinList]

j:113 [binder, in Coq.Reals.Cauchy.ConstructiveRcomplete]

j:114 [binder, in Coq.Numbers.Cyclic.Int31.Int31]

j:118 [binder, in Coq.setoid_ring.Ring_polynom]

j:119 [binder, in Coq.Numbers.Cyclic.Int63.Int63]

j:119 [binder, in Coq.Numbers.Cyclic.Int31.Int31]

j:120 [binder, in Coq.FSets.FMapPositive]

j:121 [binder, in Coq.setoid_ring.Ring_polynom]

j:122 [binder, in Coq.Numbers.Cyclic.Int31.Int31]

j:126 [binder, in Coq.micromega.EnvRing]

j:127 [binder, in Coq.Numbers.Cyclic.Int31.Int31]

j:129 [binder, in Coq.micromega.EnvRing]

j:13 [binder, in Coq.setoid_ring.BinList]

j:132 [binder, in Coq.Numbers.Cyclic.Int31.Int31]

j:136 [binder, in Coq.Numbers.Cyclic.Int31.Int31]

j:142 [binder, in Coq.Lists.SetoidList]

j:143 [binder, in Coq.Numbers.Cyclic.Int31.Int31]

j:150 [binder, in Coq.Numbers.Cyclic.Int31.Int31]

j:153 [binder, in Coq.setoid_ring.Ncring_polynom]

j:16 [binder, in Coq.setoid_ring.BinList]

j:16 [binder, in Coq.Numbers.Cyclic.Int63.Int63]

j:164 [binder, in Coq.Lists.SetoidList]

j:166 [binder, in Coq.Numbers.Cyclic.Int63.Int63]

j:169 [binder, in Coq.Lists.SetoidList]

j:17 [binder, in Coq.micromega.Env]

j:171 [binder, in Coq.Numbers.Cyclic.Int63.Int63]

j:173 [binder, in Coq.Lists.SetoidList]

j:174 [binder, in Coq.Numbers.Cyclic.Int63.Int63]

j:178 [binder, in Coq.Numbers.Cyclic.Int63.Int63]

j:18 [binder, in Coq.Numbers.Cyclic.Int63.Int63]

j:18 [binder, in Coq.setoid_ring.Ring_theory]

j:182 [binder, in Coq.Numbers.Cyclic.Int63.Int63]

j:184 [binder, in Coq.Lists.SetoidList]

j:185 [binder, in Coq.FSets.FMapPositive]

j:188 [binder, in Coq.Numbers.Cyclic.Int63.Int63]

j:188 [binder, in Coq.Lists.SetoidList]

j:19 [binder, in Coq.Array.PArray]

j:190 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]

j:192 [binder, in Coq.Numbers.Cyclic.Int63.Int63]

j:194 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]

j:197 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]

j:198 [binder, in Coq.Numbers.Cyclic.Int63.Int63]

j:198 [binder, in Coq.Reals.RiemannInt]

j:198 [binder, in Coq.Reals.RiemannInt_SF]

j:199 [binder, in Coq.Reals.RiemannInt_SF]

j:2 [binder, in Coq.micromega.Env]

j:2 [binder, in Coq.FSets.FMapPositive]

j:20 [binder, in Coq.micromega.Env]

j:20 [binder, in Coq.setoid_ring.Ring_theory]

j:200 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]

j:200 [binder, in Coq.Reals.RiemannInt]

j:200 [binder, in Coq.setoid_ring.Ncring]

j:202 [binder, in Coq.setoid_ring.Ncring]

j:204 [binder, in Coq.Numbers.Cyclic.Int63.Int63]

j:205 [binder, in Coq.setoid_ring.Ncring]

j:207 [binder, in Coq.setoid_ring.Ring_polynom]

j:210 [binder, in Coq.micromega.EnvRing]

j:215 [binder, in Coq.setoid_ring.Ring_polynom]

j:218 [binder, in Coq.micromega.EnvRing]

j:218 [binder, in Coq.Numbers.Cyclic.Int63.Int63]

j:220 [binder, in Coq.setoid_ring.Ring_polynom]

j:220 [binder, in Coq.Reals.RiemannInt_SF]

j:221 [binder, in Coq.Reals.RiemannInt_SF]

j:221 [binder, in Coq.micromega.ZMicromega]

j:223 [binder, in Coq.micromega.EnvRing]

j:223 [binder, in Coq.Numbers.Cyclic.Int63.Int63]

j:224 [binder, in Coq.micromega.ZMicromega]

j:225 [binder, in Coq.Numbers.Cyclic.Int63.Int63]

j:23 [binder, in Coq.setoid_ring.Ring_theory]

j:234 [binder, in Coq.MSets.MSetPositive]

j:236 [binder, in Coq.Numbers.Cyclic.Int63.Int63]

j:238 [binder, in Coq.Numbers.Cyclic.Int63.Int63]

j:238 [binder, in Coq.MSets.MSetPositive]

j:242 [binder, in Coq.MSets.MSetPositive]

j:243 [binder, in Coq.Numbers.Cyclic.Int63.Int63]

j:245 [binder, in Coq.MSets.MSetPositive]

j:252 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]

j:261 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]

j:265 [binder, in Coq.setoid_ring.Ring_polynom]

j:268 [binder, in Coq.setoid_ring.Ring_polynom]

j:277 [binder, in Coq.Numbers.Cyclic.Int63.Int63]

j:277 [binder, in Coq.MSets.MSetPositive]

j:283 [binder, in Coq.MSets.MSetPositive]

j:285 [binder, in Coq.micromega.EnvRing]

j:288 [binder, in Coq.micromega.EnvRing]

j:288 [binder, in Coq.MSets.MSetPositive]

j:291 [binder, in Coq.micromega.EnvRing]

j:291 [binder, in Coq.micromega.ZMicromega]

j:293 [binder, in Coq.MSets.MSetPositive]

j:296 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]

j:299 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]

j:302 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]

j:304 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]

j:307 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]

j:309 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]

j:310 [binder, in Coq.FSets.FSetPositive]

j:312 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]

j:314 [binder, in Coq.FSets.FSetPositive]

j:317 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]

j:318 [binder, in Coq.FSets.FSetPositive]

j:318 [binder, in Coq.FSets.FMapPositive]

j:32 [binder, in Coq.Logic.ClassicalEpsilon]

j:321 [binder, in Coq.setoid_ring.Ring_polynom]

j:321 [binder, in Coq.FSets.FSetPositive]

j:323 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]

j:327 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]

j:330 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]

j:331 [binder, in Coq.FSets.FMapPositive]

j:334 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]

j:335 [binder, in Coq.micromega.EnvRing]

j:336 [binder, in Coq.Numbers.Cyclic.Int63.Int63]

j:339 [binder, in Coq.FSets.FMapPositive]

j:340 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]

j:341 [binder, in Coq.FSets.FMapPositive]

j:343 [binder, in Coq.FSets.FMapPositive]

j:348 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]

j:348 [binder, in Coq.FSets.FMapFacts]

j:348 [binder, in Coq.Numbers.Cyclic.Int63.Int63]

j:349 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]

j:35 [binder, in Coq.setoid_ring.Ring_polynom]

j:350 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]

j:351 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]

j:352 [binder, in Coq.Numbers.Cyclic.Int63.Int63]

j:365 [binder, in Coq.FSets.FSetPositive]

j:37 [binder, in Coq.micromega.EnvRing]

j:373 [binder, in Coq.FSets.FSetPositive]

j:378 [binder, in Coq.FSets.FSetPositive]

j:38 [binder, in Coq.setoid_ring.Ring_polynom]

j:380 [binder, in Coq.Numbers.Cyclic.Int63.Int63]

j:382 [binder, in Coq.micromega.ZMicromega]

j:383 [binder, in Coq.Numbers.Cyclic.Int63.Int63]

j:383 [binder, in Coq.FSets.FSetPositive]

j:385 [binder, in Coq.Numbers.Cyclic.Int63.Int63]

j:387 [binder, in Coq.Numbers.Cyclic.Int63.Int63]

j:390 [binder, in Coq.Numbers.Cyclic.Int63.Int63]

j:390 [binder, in Coq.micromega.ZMicromega]

j:395 [binder, in Coq.Numbers.Cyclic.Int63.Int63]

j:40 [binder, in Coq.micromega.EnvRing]

j:402 [binder, in Coq.Numbers.Cyclic.Int63.Int63]

j:407 [binder, in Coq.Numbers.Cyclic.Int63.Int63]

j:415 [binder, in Coq.Numbers.Cyclic.Int63.Int63]

j:417 [binder, in Coq.FSets.FMapFacts]

j:419 [binder, in Coq.Numbers.Cyclic.Int63.Int63]

j:425 [binder, in Coq.Numbers.Cyclic.Int63.Int63]

j:433 [binder, in Coq.Numbers.Cyclic.Int63.Int63]

j:434 [binder, in Coq.Numbers.Cyclic.Int63.Int63]

j:435 [binder, in Coq.Numbers.Cyclic.Int63.Int63]

j:436 [binder, in Coq.Numbers.Cyclic.Int63.Int63]

j:449 [binder, in Coq.Numbers.Cyclic.Int63.Int63]

j:464 [binder, in Coq.Numbers.Cyclic.Int63.Int63]

j:466 [binder, in Coq.Numbers.Cyclic.Int63.Int63]

j:47 [binder, in Coq.Reals.ClassicalConstructiveReals]

j:471 [binder, in Coq.Numbers.Cyclic.Int63.Int63]

j:473 [binder, in Coq.Numbers.Cyclic.Int63.Int63]

j:478 [binder, in Coq.Numbers.Cyclic.Int63.Int63]

j:480 [binder, in Coq.Numbers.Cyclic.Int63.Int63]

j:55 [binder, in Coq.ZArith.Zpow_facts]

j:57 [binder, in Coq.FSets.FMapPositive]

j:59 [binder, in Coq.setoid_ring.Ring_polynom]

j:6 [binder, in Coq.FSets.FMapPositive]

j:61 [binder, in Coq.micromega.EnvRing]

j:64 [binder, in Coq.setoid_ring.Ring_polynom]

j:64 [binder, in Coq.FSets.FMapPositive]

j:66 [binder, in Coq.micromega.EnvRing]

j:66 [binder, in Coq.rtauto.Bintree]

j:66 [binder, in Coq.btauto.Reflect]

j:68 [binder, in Coq.FSets.FMapPositive]

j:731 [binder, in Coq.Lists.List]

j:74 [binder, in Coq.FSets.FMapPositive]

j:77 [binder, in Coq.Reals.ClassicalDedekindReals]

j:78 [binder, in Coq.Reals.Cauchy.ConstructiveRcomplete]

j:79 [binder, in Coq.FSets.FMapPositive]

j:8 [binder, in Coq.FSets.FMapPositive]

j:82 [binder, in Coq.Reals.RList]

j:85 [binder, in Coq.MSets.MSetProperties]

j:85 [binder, in Coq.FSets.FSetProperties]

j:854 [binder, in Coq.Lists.List]

j:858 [binder, in Coq.Lists.List]

j:87 [binder, in Coq.FSets.FMapPositive]

j:91 [binder, in Coq.FSets.FMapPositive]

j:95 [binder, in Coq.ZArith.Int]

j:95 [binder, in Coq.FSets.FMapPositive]

j:97 [binder, in Coq.ZArith.Int]

j:98 [binder, in Coq.Numbers.Cyclic.Int31.Int31]

j:99 [binder, in Coq.FSets.FMapPositive]

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 | (69982 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 | (1000 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 | (45451 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 | (770 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 | (1516 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 | (577 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 | (11564 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 | (981 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 | (622 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 | (299 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 | (472 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 | (482 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 | (843 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 | (1156 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 | (4086 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 | (163 entries) |