%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : SEV664+1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n012.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Tue May 5 06:54:46 PM UTC 2026 % Result : Theorem 86.95s 11.92s % Output : Proof 212.20s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.06 % Problem : SEV664+1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.07 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.06/0.25 % Computer : n012.cluster.edu % 0.06/0.25 % Model : x86_64 x86_64 % 0.06/0.25 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.06/0.25 % Memory : 8042.1875MB % 0.06/0.25 % OS : Linux 3.10.0-693.el7.x86_64 % 0.06/0.25 % CPULimit : 300 % 0.06/0.25 % WCLimit : 300 % 0.06/0.25 % DateTime : Tue May 5 07:54:30 EDT 2026 % 0.06/0.25 % CPUTime : % 0.16/0.43 ________ _____ % 0.16/0.43 ___ __ \_________(_)________________________________ % 0.16/0.43 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.16/0.43 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.16/0.43 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.16/0.43 % 0.16/0.43 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.16/0.43 (2023-06-19) % 0.16/0.43 % 0.16/0.43 (c) Philipp Rümmer, 2009-2023 % 0.16/0.43 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.16/0.43 Amanda Stjerna. % 0.16/0.43 Free software under BSD-3-Clause. % 0.16/0.43 % 0.16/0.43 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.16/0.43 % 0.16/0.43 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.39/0.44 Running up to 7 provers in parallel. % 0.39/0.45 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.39/0.45 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.39/0.45 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.39/0.45 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.39/0.45 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.39/0.45 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.39/0.45 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 31.74/4.88 Prover 4: Preprocessing ... % 31.74/4.88 Prover 1: Preprocessing ... % 31.74/4.89 Prover 0: Preprocessing ... % 31.74/4.89 Prover 5: Preprocessing ... % 32.45/4.93 Prover 3: Preprocessing ... % 32.45/5.01 Prover 2: Preprocessing ... % 33.35/5.04 Prover 6: Preprocessing ... % 86.15/11.85 Prover 5: Constructing countermodel ... % 86.95/11.92 Prover 5: proved (11465ms) % 86.95/11.92 % 86.95/11.92 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 86.95/11.92 % 86.95/11.92 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 107.86/14.61 Prover 3: Constructing countermodel ... % 107.86/14.62 Prover 3: stopped % 107.86/14.62 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 112.51/15.27 Prover 1: Warning: ignoring some quantifiers % 114.83/15.57 Prover 7: Preprocessing ... % 115.62/15.65 Prover 6: Constructing countermodel ... % 115.62/15.66 Prover 6: stopped % 116.39/15.73 Prover 1: Constructing countermodel ... % 116.39/15.73 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 116.39/15.74 Prover 1: Found proof (size 1) % 116.39/15.74 Prover 1: proved (15296ms) % 123.21/16.64 Prover 7: stopped % 127.80/17.21 Prover 8: Preprocessing ... % 143.17/19.23 Prover 10: Preprocessing ... % 147.66/19.80 Prover 10: stopped % 159.18/21.96 Prover 8: Warning: ignoring some quantifiers % 161.21/22.20 Prover 8: Constructing countermodel ... % 161.21/22.20 Prover 8: stopped % 172.38/24.27 Prover 2: stopped % 206.76/37.46 Prover 4: stopped % 211.97/41.50 Prover 0: stopped % 211.97/41.50 % 211.97/41.51 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 211.97/41.51 % 211.97/41.51 % SZS output start Proof for theBenchmark % 211.97/41.57 Assumptions after simplification: % 211.97/41.57 --------------------------------- % 211.97/41.57 % 211.97/41.57 (_HAMMER_GOAL) % 211.97/41.57 $false % 211.97/41.57 % 211.97/41.57 Further assumptions not needed in the proof: % 211.97/41.57 -------------------------------------------- % 211.97/41.58 $_case_Coq.Init.Datatypes.bool$102739, $_case_Coq.Init.Datatypes.bool$142229, % 211.97/41.58 $_case_Coq.Init.Datatypes.comparison$165612, % 211.97/41.58 $_case_Coq.Init.Datatypes.nat$21811, $_case_Coq.Init.Datatypes.nat$21833, % 211.97/41.58 $_case_Coq.Init.Datatypes.prod$8582, $_case_Coq.Numbers.BinNums.Z$21828, % 211.97/41.58 $_def_$_let_var_6_p_21874_21877, $_def_$_let_var_6_p_21876_21878, % 211.97/41.58 $_def_Coq.Arith.EqNat.eq_nat, $_def_Coq.Arith.PeanoNat.Nat.b2n, % 211.97/41.58 $_def_Coq.Arith.PeanoNat.Nat.divide, $_def_Coq.Arith.PeanoNat.Nat.eqf, % 211.97/41.58 $_def_Coq.Bool.Bool.Is_true, $_def_Coq.Bool.Bool.eqb, % 211.97/41.58 $_def_Coq.Bool.Zerob.zerob, $_def_Coq.FSets.FSetPositive.PositiveSet.Equal, % 211.97/41.58 $_def_Coq.FSets.FSetPositive.PositiveSet.Exists, % 211.97/41.58 $_def_Coq.FSets.FSetPositive.PositiveSet.For_all, % 211.97/41.58 $_def_Coq.FSets.FSetPositive.PositiveSet.In, % 211.97/41.58 $_def_Coq.FSets.FSetPositive.PositiveSet.Subset, % 211.97/41.58 $_def_Coq.FSets.FSetPositive.PositiveSet.elt, % 211.97/41.58 $_def_Coq.FSets.FSetPositive.PositiveSet.empty, % 211.97/41.58 $_def_Coq.FSets.FSetPositive.PositiveSet.eq, % 211.97/41.58 $_def_Coq.FSets.FSetPositive.PositiveSet.equal, % 211.97/41.58 $_def_Coq.FSets.FSetPositive.PositiveSet.is_empty, % 211.97/41.58 $_def_Coq.FSets.FSetPositive.PositiveSet.mem, % 211.97/41.58 $_def_Coq.FSets.FSetPositive.PositiveSet.rev_append, % 211.97/41.58 $_def_Coq.FSets.FSetPositive.PositiveSet.t, $_def_Coq.Init.Datatypes.CompOpp, % 211.97/41.58 $_def_Coq.Init.Datatypes.CompSpecT, $_def_Coq.Init.Datatypes.IDProp, % 211.97/41.58 $_def_Coq.Init.Datatypes.andb, $_def_Coq.Init.Datatypes.app, % 211.97/41.58 $_def_Coq.Init.Datatypes.fst, $_def_Coq.Init.Datatypes.length, % 211.97/41.58 $_def_Coq.Init.Datatypes.negb, $_def_Coq.Init.Datatypes.orb, % 211.97/41.58 $_def_Coq.Init.Datatypes.snd, $_def_Coq.Init.Datatypes.xorb, % 211.97/41.58 $_def_Coq.Init.Nat.add, $_def_Coq.Init.Nat.compare, $_def_Coq.Init.Nat.div, % 211.97/41.58 $_def_Coq.Init.Nat.div2, $_def_Coq.Init.Nat.double, $_def_Coq.Init.Nat.eqb, % 211.97/41.58 $_def_Coq.Init.Nat.even, $_def_Coq.Init.Nat.gcd, $_def_Coq.Init.Nat.max, % 211.97/41.58 $_def_Coq.Init.Nat.min, $_def_Coq.Init.Nat.mul, $_def_Coq.Init.Nat.odd, % 211.97/41.58 $_def_Coq.Init.Nat.pow, $_def_Coq.Init.Nat.pred, $_def_Coq.Init.Nat.shiftl, % 211.97/41.58 $_def_Coq.Init.Nat.sqrt, $_def_Coq.Init.Nat.sqrt_iter, $_def_Coq.Init.Nat.sub, % 211.97/41.58 $_def_Coq.Init.Nat.testbit, $_def_Coq.Init.Peano.gt, $_def_Coq.Init.Peano.lt, % 211.97/41.58 $_def_Coq.Init.Specif.proj1_sig, $_def_Coq.Init.Specif.projT1, % 211.97/41.58 $_def_Coq.Init.Specif.projT2, $_def_Coq.Init.Wf.well_founded, % 211.97/41.58 $_def_Coq.Lists.List.In, $_def_Coq.Lists.List.fold_left, % 211.97/41.58 $_def_Coq.Lists.List.fold_right, $_def_Coq.Lists.List.last, % 211.97/41.58 $_def_Coq.Lists.List.map, $_def_Coq.Lists.List.nth, % 211.97/41.58 $_def_Coq.Lists.SetoidList.compat_bool, $_def_Coq.Lists.SetoidList.compat_op, % 211.97/41.58 $_def_Coq.Lists.SetoidList.transpose, $_def_Coq.Logic.Decidable.decidable, % 211.97/41.58 $_def_Coq.Logic.EqdepFacts.Eq_dep_eq_on, $_def_Coq.Logic.EqdepFacts.Eq_rect_eq, % 211.97/41.58 $_def_Coq.Logic.EqdepFacts.Eq_rect_eq_on, % 211.97/41.58 $_def_Coq.Logic.EqdepFacts.Streicher_K_on_, $_def_Coq.Logic.EqdepFacts.UIP_, % 211.97/41.58 $_def_Coq.Logic.EqdepFacts.UIP_on_, $_def_Coq.Logic.EqdepFacts.UIP_refl_on_, % 211.97/41.58 $_def_Coq.NArith.BinNat.N.b2n, $_def_Coq.NArith.BinNat.N.divide, % 211.97/41.58 $_def_Coq.NArith.BinNat.N.eqf, $_def_Coq.NArith.BinNat.N.le, % 211.97/41.58 $_def_Coq.NArith.BinNat.N.lt, $_def_Coq.NArith.BinNatDef.N.add, % 211.97/41.58 $_def_Coq.NArith.BinNatDef.N.compare, $_def_Coq.NArith.BinNatDef.N.div, % 211.97/41.58 $_def_Coq.NArith.BinNatDef.N.div2, $_def_Coq.NArith.BinNatDef.N.double, % 211.97/41.58 $_def_Coq.NArith.BinNatDef.N.eqb, $_def_Coq.NArith.BinNatDef.N.even, % 211.97/41.58 $_def_Coq.NArith.BinNatDef.N.gcd, $_def_Coq.NArith.BinNatDef.N.log2, % 211.97/41.58 $_def_Coq.NArith.BinNatDef.N.max, $_def_Coq.NArith.BinNatDef.N.min, % 211.97/41.58 $_def_Coq.NArith.BinNatDef.N.modulo, $_def_Coq.NArith.BinNatDef.N.mul, % 211.97/41.58 $_def_Coq.NArith.BinNatDef.N.odd, $_def_Coq.NArith.BinNatDef.N.pow, % 211.97/41.58 $_def_Coq.NArith.BinNatDef.N.pred, $_def_Coq.NArith.BinNatDef.N.sqrt, % 211.97/41.58 $_def_Coq.NArith.BinNatDef.N.sub, $_def_Coq.NArith.BinNatDef.N.succ, % 211.97/41.58 $_def_Coq.NArith.BinNatDef.N.succ_double, $_def_Coq.NArith.BinNatDef.N.testbit, % 211.97/41.58 $_def_Coq.NArith.BinNatDef.N.to_nat, $_def_Coq.PArith.BinPos.Pos.le, % 211.97/41.58 $_def_Coq.PArith.BinPos.Pos.lt, $_def_Coq.PArith.BinPos.Pos.switch_Eq, % 211.97/41.58 $_def_Coq.PArith.BinPosDef.Pos.add, $_def_Coq.PArith.BinPosDef.Pos.compare, % 211.97/41.58 $_def_Coq.PArith.BinPosDef.Pos.iter, $_def_Coq.PArith.BinPosDef.Pos.iter_op, % 211.97/41.58 $_def_Coq.PArith.BinPosDef.Pos.max, $_def_Coq.PArith.BinPosDef.Pos.min, % 211.97/41.58 $_def_Coq.PArith.BinPosDef.Pos.mul, $_def_Coq.PArith.BinPosDef.Pos.of_nat, % 211.97/41.58 $_def_Coq.PArith.BinPosDef.Pos.of_succ_nat, $_def_Coq.PArith.BinPosDef.Pos.pred, % 211.97/41.58 $_def_Coq.PArith.BinPosDef.Pos.sub, $_def_Coq.PArith.BinPosDef.Pos.succ, % 211.97/41.58 $_def_Coq.PArith.BinPosDef.Pos.to_nat, $_def_Coq.QArith.QArith_base.Qden, % 211.97/41.58 $_def_Coq.QArith.QArith_base.Qnum, $_def_Coq.Reals.RIneq.Rsqr, % 211.97/41.58 $_def_Coq.Reals.Rdefinitions.IZR, $_def_Coq.Reals.Rdefinitions.Rdiv, % 211.97/41.58 $_def_Coq.Reals.Rdefinitions.Rge, $_def_Coq.Reals.Rdefinitions.Rgt, % 211.97/41.58 $_def_Coq.Reals.Rdefinitions.Rle, $_def_Coq.Reals.Rdefinitions.Rminus, % 211.97/41.58 $_def_Coq.Reals.Rpow_def.pow, $_def_Coq.Relations.Relation_Definitions.relation, % 211.97/41.58 $_def_Coq.Setoids.Setoid.Setoid_Theory, % 211.97/41.58 $_def_Coq.Structures.OrderedTypeEx.N_as_OT.eq, % 211.97/41.58 $_def_Coq.Structures.OrderedTypeEx.N_as_OT.lt, % 211.97/41.58 $_def_Coq.Structures.OrderedTypeEx.N_as_OT.t, % 211.97/41.58 $_def_Coq.Structures.OrderedTypeEx.Nat_as_OT.eq, % 211.97/41.58 $_def_Coq.Structures.OrderedTypeEx.Nat_as_OT.lt, % 211.97/41.58 $_def_Coq.Structures.OrderedTypeEx.Nat_as_OT.t, % 211.97/41.58 $_def_Coq.Structures.OrderedTypeEx.PositiveOrderedTypeBits.eq, % 211.97/41.58 $_def_Coq.Structures.OrderedTypeEx.PositiveOrderedTypeBits.t, % 211.97/41.58 $_def_Coq.Structures.OrderedTypeEx.Positive_as_OT.eq, % 211.97/41.58 $_def_Coq.Structures.OrderedTypeEx.Positive_as_OT.lt, % 211.97/41.58 $_def_Coq.Structures.OrderedTypeEx.Positive_as_OT.t, % 211.97/41.58 $_def_Coq.Structures.OrderedTypeEx.String_as_OT.eq, % 211.97/41.58 $_def_Coq.Structures.OrderedTypeEx.String_as_OT.lt, % 211.97/41.58 $_def_Coq.Structures.OrderedTypeEx.String_as_OT.t, % 211.97/41.58 $_def_Coq.Structures.OrderedTypeEx.Z_as_OT.eq, % 211.97/41.58 $_def_Coq.Structures.OrderedTypeEx.Z_as_OT.lt, % 211.97/41.58 $_def_Coq.Structures.OrderedTypeEx.Z_as_OT.t, % 211.97/41.58 $_def_Coq.Vectors.VectorDef.fold_right, $_def_Coq.ZArith.BinInt.Z.Bezout, % 211.97/41.58 $_def_Coq.ZArith.BinInt.Z.b2z, $_def_Coq.ZArith.BinInt.Z.divide, % 211.97/41.58 $_def_Coq.ZArith.BinInt.Z.eqf, $_def_Coq.ZArith.BinInt.Z.ge, % 211.97/41.58 $_def_Coq.ZArith.BinInt.Z.gt, $_def_Coq.ZArith.BinInt.Z.le, % 211.97/41.58 $_def_Coq.ZArith.BinInt.Z.lt, $_def_Coq.ZArith.BinInt.Zne, % 211.97/41.58 $_def_Coq.ZArith.BinIntDef.Z.abs, $_def_Coq.ZArith.BinIntDef.Z.add, % 211.97/41.58 $_def_Coq.ZArith.BinIntDef.Z.compare, $_def_Coq.ZArith.BinIntDef.Z.div, % 211.97/41.58 $_def_Coq.ZArith.BinIntDef.Z.eqb, $_def_Coq.ZArith.BinIntDef.Z.gcd, % 211.97/41.58 $_def_Coq.ZArith.BinIntDef.Z.leb, $_def_Coq.ZArith.BinIntDef.Z.log2, % 211.97/41.58 $_def_Coq.ZArith.BinIntDef.Z.max, $_def_Coq.ZArith.BinIntDef.Z.min, % 211.97/41.58 $_def_Coq.ZArith.BinIntDef.Z.modulo, $_def_Coq.ZArith.BinIntDef.Z.mul, % 211.97/41.58 $_def_Coq.ZArith.BinIntDef.Z.of_N, $_def_Coq.ZArith.BinIntDef.Z.of_nat, % 211.97/41.58 $_def_Coq.ZArith.BinIntDef.Z.opp, $_def_Coq.ZArith.BinIntDef.Z.pow, % 211.97/41.58 $_def_Coq.ZArith.BinIntDef.Z.pred, $_def_Coq.ZArith.BinIntDef.Z.quot, % 211.97/41.58 $_def_Coq.ZArith.BinIntDef.Z.rem, $_def_Coq.ZArith.BinIntDef.Z.sgn, % 211.97/41.58 $_def_Coq.ZArith.BinIntDef.Z.sqrt, $_def_Coq.ZArith.BinIntDef.Z.sub, % 211.97/41.58 $_def_Coq.ZArith.BinIntDef.Z.succ, $_def_Coq.ZArith.BinIntDef.Z.to_pos, % 211.97/41.58 $_def_Coq.ZArith.Zbool.Zeq_bool, $_def_Coq.ZArith.Zdiv.Remainder, % 211.97/41.58 $_def_Coq.micromega.Env.Env, $_def_Coq.micromega.Env.jump, % 211.97/41.58 $_def_Coq.micromega.Env.nth, $_def_Coq.micromega.Refl.make_conj, % 211.97/41.58 $_def_Coq.micromega.Refl.make_impl, $_def_Coq.micromega.RingMicromega.PolEnv, % 211.97/41.58 $_def_Coq.micromega.RingMicromega.eval_op2, % 211.97/41.58 $_def_Coq.micromega.ZMicromega.Vars.Facts.Add, % 211.97/41.58 $_def_Coq.setoid_ring.Field_theory.Fapp, % 211.97/41.58 $_def_Coq.setoid_ring.Field_theory.condition, % 211.97/41.58 $_def_Coq.setoid_ring.Field_theory.denum, % 211.97/41.58 $_def_Coq.setoid_ring.Field_theory.num, % 211.97/41.58 $_def_Coq.setoid_ring.Field_theory.rsplit_left, % 211.97/41.58 $_def_Coq.setoid_ring.Field_theory.rsplit_right, % 211.97/41.58 $_def_Coq.setoid_ring.InitialRing.Nopp, $_def_Coq.setoid_ring.InitialRing.Nsub, % 211.97/41.58 $_def_Coq.setoid_ring.InitialRing.gen_phiN, % 211.97/41.58 $_def_Coq.setoid_ring.InitialRing.gen_phiZ, % 211.97/41.58 $_def_Coq.setoid_ring.InitialRing.triv_div, $_def_Coq.setoid_ring.Ring.bool_eq, % 211.97/41.58 $_def_Coq.setoid_ring.Ring_polynom.PEeval, % 211.97/41.58 $_def_Coq.setoid_ring.Ring_polynom.Peq, % 211.97/41.58 $_def_Coq.setoid_ring.Ring_tac.ring_subst_niter, % 211.97/41.58 $_def_Coq.setoid_ring.Ring_theory.IDphi, % 211.97/41.58 $_def_Coq.setoid_ring.Ring_theory.SRopp, % 211.97/41.58 $_def_Coq.setoid_ring.Ring_theory.SRsub, % 211.97/41.58 $_def_Coq.setoid_ring.Ring_theory.get_sign_None, % 211.97/41.58 $_def_Coq.setoid_ring.Ring_theory.id_phi_N, % 211.97/41.58 $_def_Coq.setoid_ring.Ring_theory.pow_N, % 211.97/41.58 $_def_Coq.setoid_ring.Ring_theory.pow_pos, % 211.97/41.58 $_discrim_Coq.Bool.Bool.ReflectT$Coq.Bool.Bool.ReflectF, % 211.97/41.58 $_discrim_Coq.FSets.FSetPositive.PositiveSet.Leaf$Coq.FSets.FSetPositive.PositiveSet.Node, % 211.97/41.58 $_discrim_Coq.Init.Byte.x00$Coq.Init.Byte.x01, % 211.97/41.58 $_discrim_Coq.Init.Datatypes.CompEqT$Coq.Init.Datatypes.CompLtT, % 211.97/41.58 $_discrim_Coq.Init.Datatypes.Eq$Coq.Init.Datatypes.Lt, % 211.97/41.58 $_discrim_Coq.Init.Datatypes.O$Coq.Init.Datatypes.S, % 211.97/41.58 $_discrim_Coq.Init.Datatypes.Some$Coq.Init.Datatypes.None, % 211.97/41.58 $_discrim_Coq.Init.Datatypes.inl$Coq.Init.Datatypes.inr, % 211.97/41.58 $_discrim_Coq.Init.Datatypes.nil$Coq.Init.Datatypes.cons, % 211.97/41.58 $_discrim_Coq.Init.Datatypes.true$Coq.Init.Datatypes.false, % 211.97/41.58 $_discrim_Coq.Init.Specif.inleft$Coq.Init.Specif.inright, % 211.97/41.58 $_discrim_Coq.Init.Specif.left$Coq.Init.Specif.right, % 211.97/41.58 $_discrim_Coq.Numbers.BinNums.N0$Coq.Numbers.BinNums.Npos, % 211.97/41.58 $_discrim_Coq.Numbers.BinNums.Z0$Coq.Numbers.BinNums.Zpos, % 211.97/41.58 $_discrim_Coq.Numbers.BinNums.xI$Coq.Numbers.BinNums.xO, % 211.97/41.58 $_discrim_Coq.PArith.BinPosDef.Pos.IsNul$Coq.PArith.BinPosDef.Pos.IsPos, % 211.97/41.58 $_discrim_Coq.Reals.Rfunctions.ZintNull$Coq.Reals.Rfunctions.ZintPos, % 211.97/41.58 $_discrim_Coq.Strings.String.EmptyString$Coq.Strings.String.String, % 211.97/41.58 $_discrim_Coq.Structures.OrderedType.LT$Coq.Structures.OrderedType.EQ, % 211.97/41.58 $_discrim_Coq.Structures.OrdersTac.OEQ$Coq.Structures.OrdersTac.OLT, % 211.97/41.58 $_discrim_Coq.Vectors.Fin.F1$Coq.Vectors.Fin.FS, % 211.97/41.58 $_discrim_Coq.Vectors.VectorDef.nil$Coq.Vectors.VectorDef.cons, % 211.97/41.58 $_discrim_Coq.micromega.EnvRing.PEc$Coq.micromega.EnvRing.PEX, % 211.97/41.58 $_discrim_Coq.micromega.EnvRing.Pc$Coq.micromega.EnvRing.Pinj, % 211.97/41.58 $_discrim_Coq.micromega.EnvRing.mon0$Coq.micromega.EnvRing.zmon, % 211.97/41.58 $_discrim_Coq.micromega.RingMicromega.Equal$Coq.micromega.RingMicromega.NonEqual, % 211.97/41.58 $_discrim_Coq.micromega.RingMicromega.OpEq$Coq.micromega.RingMicromega.OpNEq, % 211.97/41.58 $_discrim_Coq.micromega.Tauto.TT$Coq.micromega.Tauto.FF, % 211.97/41.58 $_discrim_Coq.setoid_ring.Field_theory.FEO$Coq.setoid_ring.Field_theory.FEI, % 211.97/41.58 $_discrim_Coq.setoid_ring.Ring_polynom.PEO$Coq.setoid_ring.Ring_polynom.PEI, % 211.97/41.58 $_discrim_Coq.setoid_ring.Ring_polynom.Pc$Coq.setoid_ring.Ring_polynom.Pinj, % 211.97/41.58 $_discrim_Coq.setoid_ring.Ring_polynom.mon0$Coq.setoid_ring.Ring_polynom.zmon, % 211.97/41.58 $_discrim_Coq.setoid_ring.Ring_theory.Abstract$Coq.setoid_ring.Ring_theory.Computational, % 211.97/41.58 $_fix_20500_1_add_carry, $_inj_Coq.Bool.Bool.ReflectF, % 211.97/41.58 $_inj_Coq.Bool.Bool.ReflectT, $_inj_Coq.FSets.FSetPositive.PositiveSet.Node, % 211.97/41.58 $_inj_Coq.Init.Datatypes.CompEqT, $_inj_Coq.Init.Datatypes.CompGtT, % 211.97/41.58 $_inj_Coq.Init.Datatypes.CompLtT, $_inj_Coq.Init.Datatypes.None, % 211.97/41.58 $_inj_Coq.Init.Datatypes.S, $_inj_Coq.Init.Datatypes.Some, % 211.97/41.58 $_inj_Coq.Init.Datatypes.cons, $_inj_Coq.Init.Datatypes.inl, % 211.97/41.58 $_inj_Coq.Init.Datatypes.inr, $_inj_Coq.Init.Datatypes.nil, % 211.97/41.58 $_inj_Coq.Init.Datatypes.pair, $_inj_Coq.Init.Specif.exist, % 211.97/41.58 $_inj_Coq.Init.Specif.exist2, $_inj_Coq.Init.Specif.existT, % 211.97/41.58 $_inj_Coq.Init.Specif.existT2, $_inj_Coq.Init.Specif.inleft, % 211.97/41.58 $_inj_Coq.Init.Specif.inright, $_inj_Coq.Init.Specif.left, % 211.97/41.58 $_inj_Coq.Init.Specif.right, $_inj_Coq.Numbers.BinNums.Npos, % 211.97/41.58 $_inj_Coq.Numbers.BinNums.Zneg, $_inj_Coq.Numbers.BinNums.Zpos, % 211.97/41.58 $_inj_Coq.Numbers.BinNums.xI, $_inj_Coq.Numbers.BinNums.xO, % 211.97/41.58 $_inj_Coq.PArith.BinPosDef.Pos.IsPos, $_inj_Coq.QArith.QArith_base.Qmake, % 211.97/41.58 $_inj_Coq.Reals.RIneq.mknonzeroreal, $_inj_Coq.Reals.Rfunctions.ZintNeg, % 211.97/41.58 $_inj_Coq.Reals.Rfunctions.ZintNull, $_inj_Coq.Reals.Rfunctions.ZintPos, % 211.97/41.58 $_inj_Coq.Strings.Ascii.Ascii, $_inj_Coq.Strings.String.String, % 211.97/41.58 $_inj_Coq.Structures.OrderedType.EQ, $_inj_Coq.Structures.OrderedType.GT, % 211.97/41.58 $_inj_Coq.Structures.OrderedType.LT, $_inj_Coq.Vectors.Fin.F1, % 211.97/41.58 $_inj_Coq.Vectors.Fin.FS, $_inj_Coq.Vectors.VectorDef.cons, % 211.97/41.58 $_inj_Coq.Vectors.VectorDef.nil, $_inj_Coq.ZArith.Znumtheory.Euclid_intro, % 211.97/41.58 $_inj_Coq.ZArith.Zpower.Zdiv_rest_proof, $_inj_Coq.micromega.EnvRing.PEX, % 211.97/41.58 $_inj_Coq.micromega.EnvRing.PEadd, $_inj_Coq.micromega.EnvRing.PEc, % 211.97/41.58 $_inj_Coq.micromega.EnvRing.PEmul, $_inj_Coq.micromega.EnvRing.PEopp, % 211.97/41.58 $_inj_Coq.micromega.EnvRing.PEpow, $_inj_Coq.micromega.EnvRing.PEsub, % 211.97/41.58 $_inj_Coq.micromega.EnvRing.PX, $_inj_Coq.micromega.EnvRing.Pc, % 211.97/41.58 $_inj_Coq.micromega.EnvRing.Pinj, $_inj_Coq.micromega.EnvRing.vmon, % 211.97/41.58 $_inj_Coq.micromega.EnvRing.zmon, % 211.97/41.58 $_inj_Coq.micromega.RingMicromega.Build_Formula, $_inj_Coq.micromega.Tauto.A, % 211.97/41.58 $_inj_Coq.micromega.Tauto.Cj, $_inj_Coq.micromega.Tauto.D, % 211.97/41.58 $_inj_Coq.micromega.Tauto.FF, $_inj_Coq.micromega.Tauto.I, % 211.97/41.58 $_inj_Coq.micromega.Tauto.N, $_inj_Coq.micromega.Tauto.TT, % 211.97/41.58 $_inj_Coq.micromega.Tauto.X, $_inj_Coq.setoid_ring.Field_theory.FEI, % 211.97/41.58 $_inj_Coq.setoid_ring.Field_theory.FEO, $_inj_Coq.setoid_ring.Field_theory.FEX, % 211.97/41.58 $_inj_Coq.setoid_ring.Field_theory.FEadd, % 211.97/41.58 $_inj_Coq.setoid_ring.Field_theory.FEc, % 211.97/41.58 $_inj_Coq.setoid_ring.Field_theory.FEdiv, % 211.97/41.58 $_inj_Coq.setoid_ring.Field_theory.FEinv, % 211.97/41.58 $_inj_Coq.setoid_ring.Field_theory.FEmul, % 211.97/41.58 $_inj_Coq.setoid_ring.Field_theory.FEopp, % 211.97/41.58 $_inj_Coq.setoid_ring.Field_theory.FEpow, % 211.97/41.58 $_inj_Coq.setoid_ring.Field_theory.FEsub, % 211.97/41.58 $_inj_Coq.setoid_ring.Field_theory.mk_linear, % 211.97/41.58 $_inj_Coq.setoid_ring.Field_theory.mk_rsplit, % 211.97/41.58 $_inj_Coq.setoid_ring.Ring_polynom.PEI, $_inj_Coq.setoid_ring.Ring_polynom.PEO, % 211.97/41.58 $_inj_Coq.setoid_ring.Ring_polynom.PEX, % 211.97/41.58 $_inj_Coq.setoid_ring.Ring_polynom.PEadd, % 211.97/41.58 $_inj_Coq.setoid_ring.Ring_polynom.PEc, % 211.97/41.58 $_inj_Coq.setoid_ring.Ring_polynom.PEmul, % 211.97/41.58 $_inj_Coq.setoid_ring.Ring_polynom.PEopp, % 211.97/41.58 $_inj_Coq.setoid_ring.Ring_polynom.PEpow, % 211.97/41.58 $_inj_Coq.setoid_ring.Ring_polynom.PEsub, $_inj_Coq.setoid_ring.Ring_polynom.PX, % 211.97/41.58 $_inj_Coq.setoid_ring.Ring_polynom.Pc, $_inj_Coq.setoid_ring.Ring_polynom.Pinj, % 211.97/41.58 $_inj_Coq.setoid_ring.Ring_polynom.vmon, % 211.97/41.58 $_inj_Coq.setoid_ring.Ring_polynom.zmon, % 211.97/41.58 $_inj_Coq.setoid_ring.Ring_theory.Computational, % 211.97/41.58 $_inj_Coq.setoid_ring.Ring_theory.Morphism, % 211.97/41.58 $_inversion_Coq.Arith.Between.between, $_inversion_Coq.Arith.Even.even, % 211.97/41.58 $_inversion_Coq.Arith.Even.odd, $_inversion_Coq.Bool.Bool.reflect, % 211.97/41.58 $_inversion_Coq.FSets.FSetPositive.PositiveSet.tree, % 211.97/41.58 $_inversion_Coq.Init.Byte.byte, $_inversion_Coq.Init.Datatypes.BoolSpec, % 211.97/41.58 $_inversion_Coq.Init.Datatypes.CompareSpec, % 211.97/41.58 $_inversion_Coq.Init.Datatypes.CompareSpecT, % 211.97/41.58 $_inversion_Coq.Init.Datatypes.bool, $_inversion_Coq.Init.Datatypes.comparison, % 211.97/41.58 $_inversion_Coq.Init.Datatypes.list, $_inversion_Coq.Init.Datatypes.nat, % 211.97/41.58 $_inversion_Coq.Init.Datatypes.option, $_inversion_Coq.Init.Datatypes.prod, % 211.97/41.58 $_inversion_Coq.Init.Datatypes.sum, $_inversion_Coq.Init.Datatypes.unit, % 211.97/41.58 $_inversion_Coq.Init.Peano.le, $_inversion_Coq.Init.Specif.sig, % 211.97/41.58 $_inversion_Coq.Init.Specif.sig2, $_inversion_Coq.Init.Specif.sigT, % 211.97/41.58 $_inversion_Coq.Init.Specif.sigT2, $_inversion_Coq.Init.Specif.sumbool, % 211.97/41.58 $_inversion_Coq.Init.Specif.sumor, $_inversion_Coq.Init.Wf.Acc, % 211.97/41.58 $_inversion_Coq.Lists.List.Forall, $_inversion_Coq.Lists.List.NoDup, % 211.97/41.58 $_inversion_Coq.Lists.SetoidList.InA, $_inversion_Coq.Lists.SetoidList.NoDupA, % 211.97/41.58 $_inversion_Coq.Logic.EqdepFacts.eq_dep, % 211.97/41.58 $_inversion_Coq.Logic.EqdepFacts.eq_dep1, $_inversion_Coq.Numbers.BinNums.N, % 211.97/41.58 $_inversion_Coq.Numbers.BinNums.Z, $_inversion_Coq.Numbers.BinNums.positive, % 211.97/41.58 $_inversion_Coq.PArith.BinPos.Pos.SqrtSpec, % 211.97/41.58 $_inversion_Coq.PArith.BinPos.Pos.SubMaskSpec, % 211.97/41.58 $_inversion_Coq.PArith.BinPosDef.Pos.mask, $_inversion_Coq.QArith.QArith_base.Q, % 211.97/41.58 $_inversion_Coq.Reals.RIneq.nonzeroreal, % 211.97/41.58 $_inversion_Coq.Reals.Rfunctions.Z_spec, % 211.97/41.58 $_inversion_Coq.Sorting.Sorted.StronglySorted, % 211.97/41.58 $_inversion_Coq.Strings.Ascii.ascii, $_inversion_Coq.Strings.String.string, % 211.97/41.58 $_inversion_Coq.Structures.OrderedType.Compare, % 211.97/41.58 $_inversion_Coq.Structures.OrderedTypeEx.String_as_OT.lts, % 211.97/41.58 $_inversion_Coq.Structures.OrdersTac.ord, $_inversion_Coq.Vectors.Fin.t, % 211.97/41.58 $_inversion_Coq.Vectors.VectorDef.t, $_inversion_Coq.ZArith.Znumtheory.Bezout, % 211.97/41.58 $_inversion_Coq.ZArith.Znumtheory.Euclid, % 211.97/41.58 $_inversion_Coq.ZArith.Znumtheory.Zis_gcd, % 211.97/41.58 $_inversion_Coq.ZArith.Zpower.Zdiv_rest_proofs, % 211.97/41.58 $_inversion_Coq.micromega.EnvRing.Mon, $_inversion_Coq.micromega.EnvRing.PExpr, % 211.97/41.58 $_inversion_Coq.micromega.EnvRing.Pol, % 211.97/41.58 $_inversion_Coq.micromega.OrderedRing.SOR, % 211.97/41.58 $_inversion_Coq.micromega.RingMicromega.Formula, % 211.97/41.58 $_inversion_Coq.micromega.RingMicromega.Op1, % 211.97/41.58 $_inversion_Coq.micromega.RingMicromega.Op2, % 211.97/41.58 $_inversion_Coq.micromega.RingMicromega.SORaddon, % 211.97/41.58 $_inversion_Coq.micromega.Tauto.GFormula, % 211.97/41.58 $_inversion_Coq.micromega.ZMicromega.Vars.Facts.MP.Dec.FSetDecideAuxiliary.FSet_elt_Prop, % 211.97/41.58 $_inversion_Coq.micromega.ZMicromega.is_diff_env_elt, % 211.97/41.58 $_inversion_Coq.setoid_ring.Field_theory.FExpr, % 211.97/41.58 $_inversion_Coq.setoid_ring.Field_theory.almost_field_theory, % 211.97/41.58 $_inversion_Coq.setoid_ring.Field_theory.linear, % 211.97/41.58 $_inversion_Coq.setoid_ring.Field_theory.rsplit, % 211.97/41.58 $_inversion_Coq.setoid_ring.Ring_polynom.Mon, % 211.97/41.58 $_inversion_Coq.setoid_ring.Ring_polynom.PExpr, % 211.97/41.58 $_inversion_Coq.setoid_ring.Ring_polynom.Pol, % 211.97/41.58 $_inversion_Coq.setoid_ring.Ring_theory.almost_ring_theory, % 211.97/41.58 $_inversion_Coq.setoid_ring.Ring_theory.div_theory, % 211.97/41.58 $_inversion_Coq.setoid_ring.Ring_theory.power_theory, % 211.97/41.58 $_inversion_Coq.setoid_ring.Ring_theory.ring_eq_ext, % 211.97/41.58 $_inversion_Coq.setoid_ring.Ring_theory.ring_kind, % 211.97/41.58 $_inversion_Coq.setoid_ring.Ring_theory.ring_morph, % 211.97/41.58 $_inversion_Coq.setoid_ring.Ring_theory.semi_morph, % 211.97/41.58 $_inversion_Coq.setoid_ring.Ring_theory.sign_theory, % 211.97/41.58 $_inversion_Coq.setoid_ring.Ring_theory.sring_eq_ext, $_lam_103102, $_lam_12266, % 211.97/41.58 $_lam_14771, $_lam_14779, $_lam_14787, $_lam_14795, $_prop_10581, $_prop_10582, % 211.97/41.58 $_prop_166330, $_prop_20885, $_prop_23380, $_prop_23381, $_prop_23382, % 211.97/41.58 $_prop_23383, $_prop_23384, $_prop_23385, $_prop_23386, $_prop_32246, % 211.97/41.58 $_prop_440, $_prop_441, $_type_10047, $_type_10051, $_type_10055, $_type_10101, % 211.97/41.58 $_type_10113, $_type_10125, $_type_10127, $_type_10132, $_type_101786, % 211.97/41.58 $_type_10187, $_type_10200, $_type_10202, $_type_1022, $_type_10221, % 211.97/41.58 $_type_102742, $_type_102836, $_type_103177, $_type_103179, $_type_10574, % 211.97/41.58 $_type_10579, $_type_10585, $_type_1104, $_type_11789, $_type_11847, % 211.97/41.58 $_type_11910, $_type_1197, $_type_12041, $_type_12066, $_type_12105, % 211.97/41.58 $_type_12109, $_type_12123, $_type_12222, $_type_12237, $_type_12251, % 211.97/41.58 $_type_12719, $_type_1279, $_type_12820, $_type_12921, $_type_13011, % 211.97/41.58 $_type_13112, $_type_13213, $_type_13314, $_type_13480, $_type_13499, % 211.97/41.58 $_type_13519, $_type_13622, $_type_13632, $_type_13638, $_type_13651, % 211.97/41.58 $_type_13656, $_type_13667, $_type_1372, $_type_1381, $_type_13833, % 211.97/41.58 $_type_13882, $_type_1390, $_type_141300, $_type_145287, $_type_145293, % 211.97/41.58 $_type_14832, $_type_15251, $_type_15259, $_type_15262, $_type_15391, % 211.97/41.58 $_type_154381, $_type_154397, $_type_154763, $_type_155143, $_type_156168, % 211.97/41.58 $_type_156173, $_type_158368, $_type_158399, $_type_159221, $_type_159569, % 211.97/41.58 $_type_16, $_type_16600, $_type_16603, $_type_16606, $_type_166265, % 211.97/41.58 $_type_166277, $_type_166286, $_type_166294, $_type_166299, $_type_166308, % 211.97/41.58 $_type_166313, $_type_166325, $_type_166378, $_type_166386, $_type_166389, % 211.97/41.58 $_type_16640, $_type_166723, $_type_16731, $_type_16754, $_type_16777, % 211.97/41.58 $_type_16800, $_type_16818, $_type_16844, $_type_16862, $_type_17120, % 211.97/41.58 $_type_17245, $_type_17370, $_type_17495, $_type_17620, $_type_17745, % 211.97/41.58 $_type_17856, $_type_17892, $_type_17903, $_type_17934, $_type_17946, % 211.97/41.58 $_type_17988, $_type_18023, $_type_18034, $_type_18054, $_type_18058, % 211.97/41.58 $_type_18076, $_type_18093, $_type_18097, $_type_18100, $_type_18117, % 211.97/41.58 $_type_183, $_type_18407, $_type_20068, $_type_20144, $_type_20153, % 211.97/41.58 $_type_20164, $_type_20269, $_type_20462, $_type_20466, $_type_20530, % 211.97/41.58 $_type_20574, $_type_20742, $_type_2076, $_type_2081, $_type_20841, $_type_2090, % 211.97/41.58 $_type_20994, $_type_21039, $_type_2115, $_type_2135, $_type_22, $_type_22657, % 211.97/41.58 $_type_22667, $_type_22693, $_type_22701, $_type_22709, $_type_22749, % 211.97/41.58 $_type_22757, $_type_22765, $_type_22791, $_type_22874, $_type_23298, % 211.97/41.58 $_type_23408, $_type_23504, $_type_23614, $_type_23691, $_type_23696, % 211.97/41.58 $_type_23727, $_type_24, $_type_2404, $_type_24262, $_type_24608, $_type_2469, % 211.97/41.58 $_type_2493, $_type_24954, $_type_2507, $_type_2514, $_type_25277, $_type_25623, % 211.97/41.58 $_type_25969, $_type_26315, $_type_26661, $_type_27007, $_type_27330, % 211.97/41.58 $_type_27676, $_type_28022, $_type_28345, $_type_28668, $_type_29014, % 211.97/41.58 $_type_2931, $_type_29362, $_type_29371, $_type_29419, $_type_29456, % 211.97/41.58 $_type_29472, $_type_29568, $_type_29571, $_type_29693, $_type_29696, % 211.97/41.58 $_type_29701, $_type_29709, $_type_29712, $_type_29725, $_type_29734, % 211.97/41.58 $_type_29739, $_type_29742, $_type_29747, $_type_29750, $_type_29833, % 211.97/41.58 $_type_29857, $_type_29886, $_type_29893, $_type_29957, $_type_30063, % 211.97/41.58 $_type_30078, $_type_301, $_type_30661, $_type_30688, $_type_307, $_type_30714, % 211.97/41.58 $_type_31241, $_type_31363, $_type_31374, $_type_31633, $_type_31798, % 211.97/41.58 $_type_31818, $_type_31840, $_type_31858, $_type_31864, $_type_31881, % 211.97/41.58 $_type_31887, $_type_31893, $_type_31898, $_type_31901, $_type_31952, % 211.97/41.58 $_type_322, $_type_32239, $_type_32250, $_type_3227, $_type_32317, $_type_32357, % 211.97/41.58 $_type_32412, $_type_32438, $_type_32443, $_type_32451, $_type_32468, % 211.97/41.58 $_type_32472, $_type_3420, $_type_355, $_type_364, $_type_367, $_type_373, % 211.97/41.58 $_type_386, $_type_393, $_type_397, $_type_4, $_type_400, $_type_405, % 211.97/41.58 $_type_417, $_type_438, $_type_4596, $_type_462, $_type_470, $_type_4850, % 211.97/41.58 $_type_4913, $_type_493, $_type_4976, $_type_5030, $_type_5093, $_type_5300, % 211.97/41.58 $_type_5330, $_type_5354, $_type_5384, $_type_5414, $_type_5438, $_type_547, % 211.97/41.58 $_type_5471, $_type_5495, $_type_550, $_type_5522, $_type_5921, $_type_594, % 211.97/41.58 $_type_6134, $_type_6347, $_type_640, $_type_6542, $_type_6755, $_type_6968, % 211.97/41.58 $_type_7181, $_type_7394, $_type_7589, $_type_7802, $_type_7997, $_type_8139, % 211.97/41.58 $_type_8158, $_type_8172, $_type_8327, $_type_836, $_type_8377, $_type_8427, % 211.97/41.58 $_type_8469, $_type_8519, $_type_8595, $_type_8704, $_type_8748, $_type_8784, % 211.97/41.58 $_type_8828, $_type_8840, $_type_8847, $_type_8904, $_type_8909, $_type_8915, % 211.97/41.58 $_type_8935, $_type_8976, $_type_9034, $_type_9046, $_type_9212, $_type_9218, % 211.97/41.58 $_type_9228, $_type_929, $_type_99424, $_type_99548, % 211.97/41.58 $_typeof_Coq.Arith.EqNat.eq_nat, $_typeof_Coq.Arith.PeanoNat.Nat.b2n, % 211.97/41.58 $_typeof_Coq.Arith.PeanoNat.Nat.divide, $_typeof_Coq.Arith.PeanoNat.Nat.eqf, % 211.97/41.58 $_typeof_Coq.Bool.Bool.Is_true, $_typeof_Coq.Bool.Bool.eqb, % 211.97/41.58 $_typeof_Coq.Bool.Bool.reflect, $_typeof_Coq.Bool.Zerob.zerob, % 211.97/41.58 $_typeof_Coq.FSets.FSetPositive.PositiveSet.Equal, % 211.97/41.58 $_typeof_Coq.FSets.FSetPositive.PositiveSet.Exists, % 211.97/41.58 $_typeof_Coq.FSets.FSetPositive.PositiveSet.For_all, % 211.97/41.58 $_typeof_Coq.FSets.FSetPositive.PositiveSet.In, % 211.97/41.58 $_typeof_Coq.FSets.FSetPositive.PositiveSet.Leaf, % 211.97/41.58 $_typeof_Coq.FSets.FSetPositive.PositiveSet.Node, % 211.97/41.58 $_typeof_Coq.FSets.FSetPositive.PositiveSet.Subset, % 211.97/41.58 $_typeof_Coq.FSets.FSetPositive.PositiveSet.elt, % 211.97/41.58 $_typeof_Coq.FSets.FSetPositive.PositiveSet.empty, % 211.97/41.58 $_typeof_Coq.FSets.FSetPositive.PositiveSet.eq, % 211.97/41.58 $_typeof_Coq.FSets.FSetPositive.PositiveSet.equal, % 211.97/41.58 $_typeof_Coq.FSets.FSetPositive.PositiveSet.is_empty, % 211.97/41.58 $_typeof_Coq.FSets.FSetPositive.PositiveSet.mem, % 211.97/41.58 $_typeof_Coq.FSets.FSetPositive.PositiveSet.rev_append, % 211.97/41.58 $_typeof_Coq.FSets.FSetPositive.PositiveSet.t, % 211.97/41.58 $_typeof_Coq.FSets.FSetPositive.PositiveSet.tree, $_typeof_Coq.Init.Byte.byte, % 211.97/41.58 $_typeof_Coq.Init.Byte.x00, $_typeof_Coq.Init.Byte.x01, % 211.97/41.58 $_typeof_Coq.Init.Byte.x02, $_typeof_Coq.Init.Byte.x03, % 211.97/41.58 $_typeof_Coq.Init.Byte.x04, $_typeof_Coq.Init.Byte.x05, % 211.97/41.58 $_typeof_Coq.Init.Byte.x06, $_typeof_Coq.Init.Byte.x07, % 211.97/41.58 $_typeof_Coq.Init.Byte.x08, $_typeof_Coq.Init.Byte.x09, % 211.97/41.58 $_typeof_Coq.Init.Byte.x0a, $_typeof_Coq.Init.Byte.x0b, % 211.97/41.58 $_typeof_Coq.Init.Byte.x0c, $_typeof_Coq.Init.Byte.x0d, % 211.97/41.58 $_typeof_Coq.Init.Byte.x0e, $_typeof_Coq.Init.Byte.x0f, % 211.97/41.58 $_typeof_Coq.Init.Byte.x10, $_typeof_Coq.Init.Byte.x11, % 211.97/41.58 $_typeof_Coq.Init.Byte.x12, $_typeof_Coq.Init.Byte.x13, % 211.97/41.58 $_typeof_Coq.Init.Byte.x14, $_typeof_Coq.Init.Byte.x15, % 211.97/41.58 $_typeof_Coq.Init.Byte.x16, $_typeof_Coq.Init.Byte.x17, % 211.97/41.58 $_typeof_Coq.Init.Byte.x18, $_typeof_Coq.Init.Byte.x19, % 211.97/41.58 $_typeof_Coq.Init.Byte.x1a, $_typeof_Coq.Init.Byte.x1b, % 211.97/41.58 $_typeof_Coq.Init.Byte.x1c, $_typeof_Coq.Init.Byte.x1d, % 211.97/41.58 $_typeof_Coq.Init.Byte.x1e, $_typeof_Coq.Init.Byte.x1f, % 211.97/41.58 $_typeof_Coq.Init.Byte.x20, $_typeof_Coq.Init.Byte.x21, % 211.97/41.58 $_typeof_Coq.Init.Byte.x22, $_typeof_Coq.Init.Byte.x23, % 211.97/41.58 $_typeof_Coq.Init.Byte.x24, $_typeof_Coq.Init.Byte.x25, % 211.97/41.58 $_typeof_Coq.Init.Byte.x26, $_typeof_Coq.Init.Byte.x27, % 211.97/41.58 $_typeof_Coq.Init.Byte.x28, $_typeof_Coq.Init.Byte.x29, % 211.97/41.58 $_typeof_Coq.Init.Byte.x2a, $_typeof_Coq.Init.Byte.x2b, % 211.97/41.58 $_typeof_Coq.Init.Byte.x2c, $_typeof_Coq.Init.Byte.x2d, % 211.97/41.58 $_typeof_Coq.Init.Byte.x2e, $_typeof_Coq.Init.Byte.x2f, % 211.97/41.58 $_typeof_Coq.Init.Byte.x30, $_typeof_Coq.Init.Byte.x31, % 211.97/41.58 $_typeof_Coq.Init.Byte.x32, $_typeof_Coq.Init.Byte.x33, % 211.97/41.58 $_typeof_Coq.Init.Byte.x34, $_typeof_Coq.Init.Byte.x35, % 211.97/41.58 $_typeof_Coq.Init.Byte.x36, $_typeof_Coq.Init.Byte.x37, % 211.97/41.58 $_typeof_Coq.Init.Byte.x38, $_typeof_Coq.Init.Byte.x39, % 211.97/41.58 $_typeof_Coq.Init.Byte.x3a, $_typeof_Coq.Init.Byte.x3b, % 211.97/41.58 $_typeof_Coq.Init.Byte.x3c, $_typeof_Coq.Init.Byte.x3d, % 211.97/41.58 $_typeof_Coq.Init.Byte.x3e, $_typeof_Coq.Init.Byte.x3f, % 211.97/41.58 $_typeof_Coq.Init.Byte.x40, $_typeof_Coq.Init.Byte.x41, % 211.97/41.58 $_typeof_Coq.Init.Byte.x42, $_typeof_Coq.Init.Byte.x43, % 211.97/41.58 $_typeof_Coq.Init.Byte.x44, $_typeof_Coq.Init.Byte.x45, % 211.97/41.58 $_typeof_Coq.Init.Byte.x46, $_typeof_Coq.Init.Byte.x47, % 211.97/41.58 $_typeof_Coq.Init.Byte.x48, $_typeof_Coq.Init.Byte.x49, % 211.97/41.58 $_typeof_Coq.Init.Byte.x4a, $_typeof_Coq.Init.Byte.x4b, % 211.97/41.58 $_typeof_Coq.Init.Byte.x4c, $_typeof_Coq.Init.Byte.x4d, % 211.97/41.58 $_typeof_Coq.Init.Byte.x4e, $_typeof_Coq.Init.Byte.x4f, % 211.97/41.58 $_typeof_Coq.Init.Byte.x50, $_typeof_Coq.Init.Byte.x51, % 211.97/41.58 $_typeof_Coq.Init.Byte.x52, $_typeof_Coq.Init.Byte.x53, % 211.97/41.58 $_typeof_Coq.Init.Byte.x54, $_typeof_Coq.Init.Byte.x55, % 211.97/41.58 $_typeof_Coq.Init.Byte.x56, $_typeof_Coq.Init.Byte.x57, % 211.97/41.58 $_typeof_Coq.Init.Byte.x58, $_typeof_Coq.Init.Byte.x59, % 211.97/41.58 $_typeof_Coq.Init.Byte.x5a, $_typeof_Coq.Init.Byte.x5b, % 211.97/41.58 $_typeof_Coq.Init.Byte.x5c, $_typeof_Coq.Init.Byte.x5d, % 211.97/41.58 $_typeof_Coq.Init.Byte.x5e, $_typeof_Coq.Init.Byte.x5f, % 211.97/41.58 $_typeof_Coq.Init.Byte.x60, $_typeof_Coq.Init.Byte.x61, % 211.97/41.58 $_typeof_Coq.Init.Byte.x62, $_typeof_Coq.Init.Byte.x63, % 211.97/41.58 $_typeof_Coq.Init.Byte.x64, $_typeof_Coq.Init.Byte.x65, % 211.97/41.58 $_typeof_Coq.Init.Byte.x66, $_typeof_Coq.Init.Byte.x67, % 211.97/41.58 $_typeof_Coq.Init.Byte.x68, $_typeof_Coq.Init.Byte.x69, % 211.97/41.58 $_typeof_Coq.Init.Byte.x6a, $_typeof_Coq.Init.Byte.x6b, % 211.97/41.58 $_typeof_Coq.Init.Byte.x6c, $_typeof_Coq.Init.Byte.x6d, % 211.97/41.58 $_typeof_Coq.Init.Byte.x6e, $_typeof_Coq.Init.Byte.x6f, % 211.97/41.58 $_typeof_Coq.Init.Byte.x70, $_typeof_Coq.Init.Byte.x71, % 211.97/41.58 $_typeof_Coq.Init.Byte.x72, $_typeof_Coq.Init.Byte.x73, % 211.97/41.58 $_typeof_Coq.Init.Byte.x74, $_typeof_Coq.Init.Byte.x75, % 211.97/41.58 $_typeof_Coq.Init.Byte.x76, $_typeof_Coq.Init.Byte.x77, % 211.97/41.58 $_typeof_Coq.Init.Byte.x78, $_typeof_Coq.Init.Byte.x79, % 211.97/41.58 $_typeof_Coq.Init.Byte.x7a, $_typeof_Coq.Init.Byte.x7b, % 211.97/41.58 $_typeof_Coq.Init.Byte.x7c, $_typeof_Coq.Init.Byte.x7d, % 211.97/41.58 $_typeof_Coq.Init.Byte.x7e, $_typeof_Coq.Init.Byte.x7f, % 211.97/41.58 $_typeof_Coq.Init.Byte.x80, $_typeof_Coq.Init.Byte.x81, % 211.97/41.58 $_typeof_Coq.Init.Byte.x82, $_typeof_Coq.Init.Byte.x83, % 211.97/41.58 $_typeof_Coq.Init.Byte.x84, $_typeof_Coq.Init.Byte.x85, % 211.97/41.58 $_typeof_Coq.Init.Byte.x86, $_typeof_Coq.Init.Byte.x87, % 211.97/41.58 $_typeof_Coq.Init.Byte.x88, $_typeof_Coq.Init.Byte.x89, % 211.97/41.58 $_typeof_Coq.Init.Byte.x8a, $_typeof_Coq.Init.Byte.x8b, % 211.97/41.58 $_typeof_Coq.Init.Byte.x8c, $_typeof_Coq.Init.Byte.x8d, % 211.97/41.58 $_typeof_Coq.Init.Byte.x8e, $_typeof_Coq.Init.Byte.x8f, % 211.97/41.58 $_typeof_Coq.Init.Byte.x90, $_typeof_Coq.Init.Byte.x91, % 211.97/41.58 $_typeof_Coq.Init.Byte.x92, $_typeof_Coq.Init.Byte.x93, % 211.97/41.58 $_typeof_Coq.Init.Byte.x94, $_typeof_Coq.Init.Byte.x95, % 211.97/41.58 $_typeof_Coq.Init.Byte.x96, $_typeof_Coq.Init.Byte.x97, % 211.97/41.58 $_typeof_Coq.Init.Byte.x98, $_typeof_Coq.Init.Byte.x99, % 211.97/41.58 $_typeof_Coq.Init.Byte.x9a, $_typeof_Coq.Init.Byte.x9b, % 211.97/41.58 $_typeof_Coq.Init.Byte.x9c, $_typeof_Coq.Init.Byte.x9d, % 211.97/41.58 $_typeof_Coq.Init.Byte.x9e, $_typeof_Coq.Init.Byte.x9f, % 211.97/41.58 $_typeof_Coq.Init.Byte.xa0, $_typeof_Coq.Init.Byte.xa1, % 211.97/41.58 $_typeof_Coq.Init.Byte.xa2, $_typeof_Coq.Init.Byte.xa3, % 211.97/41.58 $_typeof_Coq.Init.Byte.xa4, $_typeof_Coq.Init.Byte.xa5, % 211.97/41.58 $_typeof_Coq.Init.Byte.xa6, $_typeof_Coq.Init.Byte.xa7, % 211.97/41.58 $_typeof_Coq.Init.Byte.xa8, $_typeof_Coq.Init.Byte.xa9, % 211.97/41.58 $_typeof_Coq.Init.Byte.xaa, $_typeof_Coq.Init.Byte.xab, % 211.97/41.58 $_typeof_Coq.Init.Byte.xac, $_typeof_Coq.Init.Byte.xad, % 211.97/41.58 $_typeof_Coq.Init.Byte.xae, $_typeof_Coq.Init.Byte.xaf, % 211.97/41.58 $_typeof_Coq.Init.Byte.xb0, $_typeof_Coq.Init.Byte.xb1, % 211.97/41.58 $_typeof_Coq.Init.Byte.xb2, $_typeof_Coq.Init.Byte.xb3, % 211.97/41.58 $_typeof_Coq.Init.Byte.xb4, $_typeof_Coq.Init.Byte.xb5, % 211.97/41.58 $_typeof_Coq.Init.Byte.xb6, $_typeof_Coq.Init.Byte.xb7, % 211.97/41.58 $_typeof_Coq.Init.Byte.xb8, $_typeof_Coq.Init.Byte.xb9, % 211.97/41.58 $_typeof_Coq.Init.Byte.xba, $_typeof_Coq.Init.Byte.xbb, % 211.97/41.58 $_typeof_Coq.Init.Byte.xbc, $_typeof_Coq.Init.Byte.xbd, % 211.97/41.58 $_typeof_Coq.Init.Byte.xbe, $_typeof_Coq.Init.Byte.xbf, % 211.97/41.58 $_typeof_Coq.Init.Byte.xc0, $_typeof_Coq.Init.Byte.xc1, % 211.97/41.58 $_typeof_Coq.Init.Byte.xc2, $_typeof_Coq.Init.Byte.xc3, % 211.97/41.58 $_typeof_Coq.Init.Byte.xc4, $_typeof_Coq.Init.Byte.xc5, % 211.97/41.58 $_typeof_Coq.Init.Byte.xc6, $_typeof_Coq.Init.Byte.xc7, % 211.97/41.58 $_typeof_Coq.Init.Byte.xc8, $_typeof_Coq.Init.Byte.xc9, % 211.97/41.58 $_typeof_Coq.Init.Byte.xca, $_typeof_Coq.Init.Byte.xcb, % 211.97/41.58 $_typeof_Coq.Init.Byte.xcc, $_typeof_Coq.Init.Byte.xcd, % 211.97/41.58 $_typeof_Coq.Init.Byte.xce, $_typeof_Coq.Init.Byte.xcf, % 211.97/41.58 $_typeof_Coq.Init.Byte.xd0, $_typeof_Coq.Init.Byte.xd1, % 211.97/41.58 $_typeof_Coq.Init.Byte.xd2, $_typeof_Coq.Init.Byte.xd3, % 211.97/41.58 $_typeof_Coq.Init.Byte.xd4, $_typeof_Coq.Init.Byte.xd5, % 211.97/41.58 $_typeof_Coq.Init.Byte.xd6, $_typeof_Coq.Init.Byte.xd7, % 211.97/41.58 $_typeof_Coq.Init.Byte.xd8, $_typeof_Coq.Init.Byte.xd9, % 211.97/41.58 $_typeof_Coq.Init.Byte.xda, $_typeof_Coq.Init.Byte.xdb, % 211.97/41.58 $_typeof_Coq.Init.Byte.xdc, $_typeof_Coq.Init.Byte.xdd, % 211.97/41.58 $_typeof_Coq.Init.Byte.xde, $_typeof_Coq.Init.Byte.xdf, % 211.97/41.58 $_typeof_Coq.Init.Byte.xe0, $_typeof_Coq.Init.Byte.xe1, % 211.97/41.58 $_typeof_Coq.Init.Byte.xe2, $_typeof_Coq.Init.Byte.xe3, % 211.97/41.58 $_typeof_Coq.Init.Byte.xe4, $_typeof_Coq.Init.Byte.xe5, % 211.97/41.58 $_typeof_Coq.Init.Byte.xe6, $_typeof_Coq.Init.Byte.xe7, % 211.97/41.59 $_typeof_Coq.Init.Byte.xe8, $_typeof_Coq.Init.Byte.xe9, % 211.97/41.59 $_typeof_Coq.Init.Byte.xea, $_typeof_Coq.Init.Byte.xeb, % 211.97/41.59 $_typeof_Coq.Init.Byte.xec, $_typeof_Coq.Init.Byte.xed, % 211.97/41.59 $_typeof_Coq.Init.Byte.xee, $_typeof_Coq.Init.Byte.xef, % 211.97/41.59 $_typeof_Coq.Init.Byte.xf0, $_typeof_Coq.Init.Byte.xf1, % 211.97/41.59 $_typeof_Coq.Init.Byte.xf2, $_typeof_Coq.Init.Byte.xf3, % 211.97/41.59 $_typeof_Coq.Init.Byte.xf4, $_typeof_Coq.Init.Byte.xf5, % 211.97/41.59 $_typeof_Coq.Init.Byte.xf6, $_typeof_Coq.Init.Byte.xf7, % 211.97/41.59 $_typeof_Coq.Init.Byte.xf8, $_typeof_Coq.Init.Byte.xf9, % 211.97/41.59 $_typeof_Coq.Init.Byte.xfa, $_typeof_Coq.Init.Byte.xfb, % 211.97/41.59 $_typeof_Coq.Init.Byte.xfc, $_typeof_Coq.Init.Byte.xfd, % 211.97/41.59 $_typeof_Coq.Init.Byte.xfe, $_typeof_Coq.Init.Byte.xff, % 211.97/41.59 $_typeof_Coq.Init.Datatypes.CompOpp, $_typeof_Coq.Init.Datatypes.CompSpecT, % 211.97/41.59 $_typeof_Coq.Init.Datatypes.CompareSpecT, $_typeof_Coq.Init.Datatypes.Eq, % 211.97/41.59 $_typeof_Coq.Init.Datatypes.Gt, $_typeof_Coq.Init.Datatypes.IDProp, % 211.97/41.59 $_typeof_Coq.Init.Datatypes.Lt, $_typeof_Coq.Init.Datatypes.None, % 211.97/41.59 $_typeof_Coq.Init.Datatypes.O, $_typeof_Coq.Init.Datatypes.S, % 211.97/41.59 $_typeof_Coq.Init.Datatypes.Some, $_typeof_Coq.Init.Datatypes.andb, % 211.97/41.59 $_typeof_Coq.Init.Datatypes.app, $_typeof_Coq.Init.Datatypes.bool, % 211.97/41.59 $_typeof_Coq.Init.Datatypes.comparison, $_typeof_Coq.Init.Datatypes.cons, % 211.97/41.59 $_typeof_Coq.Init.Datatypes.false, $_typeof_Coq.Init.Datatypes.fst, % 211.97/41.59 $_typeof_Coq.Init.Datatypes.length, $_typeof_Coq.Init.Datatypes.list, % 211.97/41.59 $_typeof_Coq.Init.Datatypes.nat, $_typeof_Coq.Init.Datatypes.negb, % 211.97/41.59 $_typeof_Coq.Init.Datatypes.nil, $_typeof_Coq.Init.Datatypes.option, % 211.97/41.59 $_typeof_Coq.Init.Datatypes.orb, $_typeof_Coq.Init.Datatypes.pair, % 211.97/41.59 $_typeof_Coq.Init.Datatypes.prod, $_typeof_Coq.Init.Datatypes.snd, % 211.97/41.59 $_typeof_Coq.Init.Datatypes.sum, $_typeof_Coq.Init.Datatypes.true, % 211.97/41.59 $_typeof_Coq.Init.Datatypes.tt, $_typeof_Coq.Init.Datatypes.unit, % 211.97/41.59 $_typeof_Coq.Init.Datatypes.xorb, $_typeof_Coq.Init.Nat.add, % 211.97/41.59 $_typeof_Coq.Init.Nat.compare, $_typeof_Coq.Init.Nat.div, % 211.97/41.59 $_typeof_Coq.Init.Nat.div2, $_typeof_Coq.Init.Nat.double, % 211.97/41.59 $_typeof_Coq.Init.Nat.eqb, $_typeof_Coq.Init.Nat.even, % 211.97/41.59 $_typeof_Coq.Init.Nat.gcd, $_typeof_Coq.Init.Nat.max, $_typeof_Coq.Init.Nat.min, % 211.97/41.59 $_typeof_Coq.Init.Nat.mul, $_typeof_Coq.Init.Nat.odd, $_typeof_Coq.Init.Nat.pow, % 211.97/41.59 $_typeof_Coq.Init.Nat.pred, $_typeof_Coq.Init.Nat.shiftl, % 211.97/41.59 $_typeof_Coq.Init.Nat.sqrt, $_typeof_Coq.Init.Nat.sqrt_iter, % 211.97/41.59 $_typeof_Coq.Init.Nat.sub, $_typeof_Coq.Init.Nat.testbit, % 211.97/41.59 $_typeof_Coq.Init.Peano.gt, $_typeof_Coq.Init.Peano.lt, % 211.97/41.59 $_typeof_Coq.Init.Specif.exist, $_typeof_Coq.Init.Specif.exist2, % 211.97/41.59 $_typeof_Coq.Init.Specif.existT, $_typeof_Coq.Init.Specif.existT2, % 211.97/41.59 $_typeof_Coq.Init.Specif.inleft, $_typeof_Coq.Init.Specif.inright, % 211.97/41.59 $_typeof_Coq.Init.Specif.left, $_typeof_Coq.Init.Specif.proj1_sig, % 211.97/41.59 $_typeof_Coq.Init.Specif.projT1, $_typeof_Coq.Init.Specif.projT2, % 211.97/41.59 $_typeof_Coq.Init.Specif.right, $_typeof_Coq.Init.Specif.sig, % 211.97/41.59 $_typeof_Coq.Init.Specif.sig2, $_typeof_Coq.Init.Specif.sigT, % 211.97/41.59 $_typeof_Coq.Init.Specif.sigT2, $_typeof_Coq.Init.Specif.sumbool, % 211.97/41.59 $_typeof_Coq.Init.Specif.sumor, $_typeof_Coq.Init.Wf.well_founded, % 211.97/41.59 $_typeof_Coq.Lists.List.In, $_typeof_Coq.Lists.List.fold_left, % 211.97/41.59 $_typeof_Coq.Lists.List.fold_right, $_typeof_Coq.Lists.List.last, % 211.97/41.59 $_typeof_Coq.Lists.List.map, $_typeof_Coq.Lists.List.nth, % 211.97/41.59 $_typeof_Coq.Lists.SetoidList.compat_bool, % 211.97/41.59 $_typeof_Coq.Lists.SetoidList.compat_op, % 211.97/41.59 $_typeof_Coq.Lists.SetoidList.transpose, $_typeof_Coq.Logic.Decidable.decidable, % 211.97/41.59 $_typeof_Coq.Logic.EqdepFacts.Eq_dep_eq_on, % 211.97/41.59 $_typeof_Coq.Logic.EqdepFacts.Eq_rect_eq, % 211.97/41.59 $_typeof_Coq.Logic.EqdepFacts.Eq_rect_eq_on, % 211.97/41.59 $_typeof_Coq.Logic.EqdepFacts.Streicher_K_on_, % 211.97/41.59 $_typeof_Coq.Logic.EqdepFacts.UIP_, $_typeof_Coq.Logic.EqdepFacts.UIP_on_, % 211.97/41.59 $_typeof_Coq.Logic.EqdepFacts.UIP_refl_on_, $_typeof_Coq.NArith.BinNat.N.b2n, % 211.97/41.59 $_typeof_Coq.NArith.BinNat.N.divide, $_typeof_Coq.NArith.BinNat.N.eqf, % 211.97/41.59 $_typeof_Coq.NArith.BinNat.N.le, $_typeof_Coq.NArith.BinNat.N.lt, % 211.97/41.59 $_typeof_Coq.NArith.BinNatDef.N.add, $_typeof_Coq.NArith.BinNatDef.N.compare, % 211.97/41.59 $_typeof_Coq.NArith.BinNatDef.N.div, $_typeof_Coq.NArith.BinNatDef.N.div2, % 211.97/41.59 $_typeof_Coq.NArith.BinNatDef.N.double, $_typeof_Coq.NArith.BinNatDef.N.eqb, % 211.97/41.59 $_typeof_Coq.NArith.BinNatDef.N.even, $_typeof_Coq.NArith.BinNatDef.N.gcd, % 211.97/41.59 $_typeof_Coq.NArith.BinNatDef.N.log2, $_typeof_Coq.NArith.BinNatDef.N.max, % 211.97/41.59 $_typeof_Coq.NArith.BinNatDef.N.min, $_typeof_Coq.NArith.BinNatDef.N.modulo, % 211.97/41.59 $_typeof_Coq.NArith.BinNatDef.N.mul, $_typeof_Coq.NArith.BinNatDef.N.odd, % 211.97/41.59 $_typeof_Coq.NArith.BinNatDef.N.pow, $_typeof_Coq.NArith.BinNatDef.N.pred, % 211.97/41.59 $_typeof_Coq.NArith.BinNatDef.N.sqrt, $_typeof_Coq.NArith.BinNatDef.N.sub, % 211.97/41.59 $_typeof_Coq.NArith.BinNatDef.N.succ, % 211.97/41.59 $_typeof_Coq.NArith.BinNatDef.N.succ_double, % 211.97/41.59 $_typeof_Coq.NArith.BinNatDef.N.testbit, $_typeof_Coq.NArith.BinNatDef.N.to_nat, % 211.97/41.59 $_typeof_Coq.Numbers.BinNums.N, $_typeof_Coq.Numbers.BinNums.N0, % 211.97/41.59 $_typeof_Coq.Numbers.BinNums.Npos, $_typeof_Coq.Numbers.BinNums.Z, % 211.97/41.59 $_typeof_Coq.Numbers.BinNums.Z0, $_typeof_Coq.Numbers.BinNums.Zneg, % 211.97/41.59 $_typeof_Coq.Numbers.BinNums.Zpos, $_typeof_Coq.Numbers.BinNums.positive, % 211.97/41.59 $_typeof_Coq.Numbers.BinNums.xH, $_typeof_Coq.Numbers.BinNums.xI, % 211.97/41.59 $_typeof_Coq.Numbers.BinNums.xO, $_typeof_Coq.PArith.BinPos.Pos.le, % 211.97/41.59 $_typeof_Coq.PArith.BinPos.Pos.lt, $_typeof_Coq.PArith.BinPos.Pos.switch_Eq, % 211.97/41.59 $_typeof_Coq.PArith.BinPosDef.Pos.IsNeg, % 211.97/41.59 $_typeof_Coq.PArith.BinPosDef.Pos.IsNul, % 211.97/41.59 $_typeof_Coq.PArith.BinPosDef.Pos.IsPos, $_typeof_Coq.PArith.BinPosDef.Pos.add, % 211.97/41.59 $_typeof_Coq.PArith.BinPosDef.Pos.compare, % 211.97/41.59 $_typeof_Coq.PArith.BinPosDef.Pos.iter, % 211.97/41.59 $_typeof_Coq.PArith.BinPosDef.Pos.iter_op, % 211.97/41.59 $_typeof_Coq.PArith.BinPosDef.Pos.mask, $_typeof_Coq.PArith.BinPosDef.Pos.max, % 211.97/41.59 $_typeof_Coq.PArith.BinPosDef.Pos.min, $_typeof_Coq.PArith.BinPosDef.Pos.mul, % 211.97/41.59 $_typeof_Coq.PArith.BinPosDef.Pos.of_nat, % 211.97/41.59 $_typeof_Coq.PArith.BinPosDef.Pos.of_succ_nat, % 211.97/41.59 $_typeof_Coq.PArith.BinPosDef.Pos.pred, $_typeof_Coq.PArith.BinPosDef.Pos.sub, % 211.97/41.59 $_typeof_Coq.PArith.BinPosDef.Pos.succ, % 211.97/41.59 $_typeof_Coq.PArith.BinPosDef.Pos.to_nat, $_typeof_Coq.QArith.QArith_base.Q, % 211.97/41.59 $_typeof_Coq.QArith.QArith_base.Qden, $_typeof_Coq.QArith.QArith_base.Qmake, % 211.97/41.59 $_typeof_Coq.QArith.QArith_base.Qnum, $_typeof_Coq.Reals.RIneq.Rsqr, % 211.97/41.59 $_typeof_Coq.Reals.RIneq.nonzeroreal, $_typeof_Coq.Reals.Rdefinitions.IZR, % 211.97/41.59 $_typeof_Coq.Reals.Rdefinitions.R, $_typeof_Coq.Reals.Rdefinitions.R0, % 211.97/41.59 $_typeof_Coq.Reals.Rdefinitions.Rdiv, $_typeof_Coq.Reals.Rdefinitions.Rge, % 211.97/41.59 $_typeof_Coq.Reals.Rdefinitions.Rgt, $_typeof_Coq.Reals.Rdefinitions.Rinv, % 211.97/41.59 $_typeof_Coq.Reals.Rdefinitions.Rle, $_typeof_Coq.Reals.Rdefinitions.Rlt, % 211.97/41.59 $_typeof_Coq.Reals.Rdefinitions.Rminus, $_typeof_Coq.Reals.Rdefinitions.Rmult, % 211.97/41.59 $_typeof_Coq.Reals.Rdefinitions.Ropp, $_typeof_Coq.Reals.Rdefinitions.Rplus, % 211.97/41.59 $_typeof_Coq.Reals.Rdefinitions.up, $_typeof_Coq.Reals.Rfunctions.Z_spec, % 211.97/41.59 $_typeof_Coq.Reals.Rfunctions.ZintNull, $_typeof_Coq.Reals.Rfunctions.intP, % 211.97/41.59 $_typeof_Coq.Reals.Rpow_def.pow, % 211.97/41.59 $_typeof_Coq.Relations.Relation_Definitions.relation, % 211.97/41.59 $_typeof_Coq.Setoids.Setoid.Setoid_Theory, $_typeof_Coq.Strings.Ascii.ascii, % 211.97/41.59 $_typeof_Coq.Strings.String.EmptyString, $_typeof_Coq.Strings.String.String, % 211.97/41.59 $_typeof_Coq.Strings.String.string, $_typeof_Coq.Structures.OrderedType.Compare, % 211.97/41.59 $_typeof_Coq.Structures.OrderedType.EQ, $_typeof_Coq.Structures.OrderedType.GT, % 211.97/41.59 $_typeof_Coq.Structures.OrderedType.LT, % 211.97/41.59 $_typeof_Coq.Structures.OrderedTypeEx.N_as_OT.eq, % 211.97/41.59 $_typeof_Coq.Structures.OrderedTypeEx.N_as_OT.lt, % 211.97/41.59 $_typeof_Coq.Structures.OrderedTypeEx.N_as_OT.t, % 211.97/41.59 $_typeof_Coq.Structures.OrderedTypeEx.Nat_as_OT.eq, % 211.97/41.59 $_typeof_Coq.Structures.OrderedTypeEx.Nat_as_OT.lt, % 211.97/41.59 $_typeof_Coq.Structures.OrderedTypeEx.Nat_as_OT.t, % 211.97/41.59 $_typeof_Coq.Structures.OrderedTypeEx.PositiveOrderedTypeBits.eq, % 211.97/41.59 $_typeof_Coq.Structures.OrderedTypeEx.PositiveOrderedTypeBits.eq_dec, % 211.97/41.59 $_typeof_Coq.Structures.OrderedTypeEx.PositiveOrderedTypeBits.t, % 211.97/41.59 $_typeof_Coq.Structures.OrderedTypeEx.Positive_as_OT.eq, % 211.97/41.59 $_typeof_Coq.Structures.OrderedTypeEx.Positive_as_OT.lt, % 211.97/41.59 $_typeof_Coq.Structures.OrderedTypeEx.Positive_as_OT.t, % 211.97/41.59 $_typeof_Coq.Structures.OrderedTypeEx.String_as_OT.eq, % 211.97/41.59 $_typeof_Coq.Structures.OrderedTypeEx.String_as_OT.lt, % 211.97/41.59 $_typeof_Coq.Structures.OrderedTypeEx.String_as_OT.t, % 211.97/41.59 $_typeof_Coq.Structures.OrderedTypeEx.Z_as_OT.eq, % 211.97/41.59 $_typeof_Coq.Structures.OrderedTypeEx.Z_as_OT.lt, % 211.97/41.59 $_typeof_Coq.Structures.OrderedTypeEx.Z_as_OT.t, % 211.97/41.59 $_typeof_Coq.Structures.OrdersTac.OEQ, $_typeof_Coq.Structures.OrdersTac.OLE, % 211.97/41.59 $_typeof_Coq.Structures.OrdersTac.OLT, $_typeof_Coq.Structures.OrdersTac.ord, % 211.97/41.59 $_typeof_Coq.Vectors.Fin.F1, $_typeof_Coq.Vectors.Fin.t, % 211.97/41.59 $_typeof_Coq.Vectors.VectorDef.cons, $_typeof_Coq.Vectors.VectorDef.fold_right, % 211.97/41.59 $_typeof_Coq.Vectors.VectorDef.nil, $_typeof_Coq.Vectors.VectorDef.t, % 211.97/41.59 $_typeof_Coq.ZArith.BinInt.Z.Bezout, $_typeof_Coq.ZArith.BinInt.Z.b2z, % 211.97/41.59 $_typeof_Coq.ZArith.BinInt.Z.divide, $_typeof_Coq.ZArith.BinInt.Z.eqf, % 211.97/41.59 $_typeof_Coq.ZArith.BinInt.Z.ge, $_typeof_Coq.ZArith.BinInt.Z.gt, % 211.97/41.59 $_typeof_Coq.ZArith.BinInt.Z.le, $_typeof_Coq.ZArith.BinInt.Z.lt, % 211.97/41.59 $_typeof_Coq.ZArith.BinInt.Zne, $_typeof_Coq.ZArith.BinIntDef.Z.abs, % 211.97/41.59 $_typeof_Coq.ZArith.BinIntDef.Z.add, $_typeof_Coq.ZArith.BinIntDef.Z.compare, % 211.97/41.59 $_typeof_Coq.ZArith.BinIntDef.Z.div, $_typeof_Coq.ZArith.BinIntDef.Z.eqb, % 211.97/41.59 $_typeof_Coq.ZArith.BinIntDef.Z.gcd, $_typeof_Coq.ZArith.BinIntDef.Z.leb, % 211.97/41.59 $_typeof_Coq.ZArith.BinIntDef.Z.log2, $_typeof_Coq.ZArith.BinIntDef.Z.max, % 211.97/41.59 $_typeof_Coq.ZArith.BinIntDef.Z.min, $_typeof_Coq.ZArith.BinIntDef.Z.modulo, % 211.97/41.59 $_typeof_Coq.ZArith.BinIntDef.Z.mul, $_typeof_Coq.ZArith.BinIntDef.Z.of_N, % 211.97/41.59 $_typeof_Coq.ZArith.BinIntDef.Z.of_nat, $_typeof_Coq.ZArith.BinIntDef.Z.opp, % 211.97/41.59 $_typeof_Coq.ZArith.BinIntDef.Z.pow, $_typeof_Coq.ZArith.BinIntDef.Z.pred, % 211.97/41.59 $_typeof_Coq.ZArith.BinIntDef.Z.quot, $_typeof_Coq.ZArith.BinIntDef.Z.rem, % 211.97/41.59 $_typeof_Coq.ZArith.BinIntDef.Z.sgn, $_typeof_Coq.ZArith.BinIntDef.Z.sqrt, % 211.97/41.59 $_typeof_Coq.ZArith.BinIntDef.Z.sub, $_typeof_Coq.ZArith.BinIntDef.Z.succ, % 211.97/41.59 $_typeof_Coq.ZArith.BinIntDef.Z.to_pos, $_typeof_Coq.ZArith.Zbool.Zeq_bool, % 211.97/41.59 $_typeof_Coq.ZArith.Zdiv.Remainder, $_typeof_Coq.ZArith.Znumtheory.Euclid, % 211.97/41.59 $_typeof_Coq.ZArith.Zpower.Zdiv_rest_proofs, $_typeof_Coq.micromega.Env.Env, % 211.97/41.59 $_typeof_Coq.micromega.Env.jump, $_typeof_Coq.micromega.Env.nth, % 211.97/41.59 $_typeof_Coq.micromega.EnvRing.Mon, $_typeof_Coq.micromega.EnvRing.PEX, % 211.97/41.59 $_typeof_Coq.micromega.EnvRing.PEadd, $_typeof_Coq.micromega.EnvRing.PEc, % 211.97/41.59 $_typeof_Coq.micromega.EnvRing.PEmul, $_typeof_Coq.micromega.EnvRing.PEopp, % 211.97/41.59 $_typeof_Coq.micromega.EnvRing.PEpow, $_typeof_Coq.micromega.EnvRing.PEsub, % 211.97/41.59 $_typeof_Coq.micromega.EnvRing.PExpr, $_typeof_Coq.micromega.EnvRing.PX, % 211.97/41.59 $_typeof_Coq.micromega.EnvRing.Pc, $_typeof_Coq.micromega.EnvRing.Pinj, % 211.97/41.59 $_typeof_Coq.micromega.EnvRing.Pol, $_typeof_Coq.micromega.EnvRing.mon0, % 211.97/41.59 $_typeof_Coq.micromega.EnvRing.vmon, $_typeof_Coq.micromega.EnvRing.zmon, % 211.97/41.59 $_typeof_Coq.micromega.Refl.make_conj, $_typeof_Coq.micromega.Refl.make_impl, % 211.97/41.59 $_typeof_Coq.micromega.RingMicromega.Formula, % 211.97/41.59 $_typeof_Coq.micromega.RingMicromega.Op1, % 211.97/41.59 $_typeof_Coq.micromega.RingMicromega.Op2, % 211.97/41.59 $_typeof_Coq.micromega.RingMicromega.PolEnv, % 211.97/41.59 $_typeof_Coq.micromega.RingMicromega.eval_op2, % 211.97/41.59 $_typeof_Coq.micromega.Tauto.GFormula, % 211.97/41.59 $_typeof_Coq.micromega.ZMicromega.Vars.Facts.Add, % 211.97/41.59 $_typeof_Coq.setoid_ring.Field_theory.FEX, % 211.97/41.59 $_typeof_Coq.setoid_ring.Field_theory.FEc, % 211.97/41.59 $_typeof_Coq.setoid_ring.Field_theory.FEinv, % 211.97/41.59 $_typeof_Coq.setoid_ring.Field_theory.FEmul, % 211.97/41.59 $_typeof_Coq.setoid_ring.Field_theory.FEopp, % 211.97/41.59 $_typeof_Coq.setoid_ring.Field_theory.FExpr, % 211.97/41.59 $_typeof_Coq.setoid_ring.Field_theory.Fapp, % 211.97/41.59 $_typeof_Coq.setoid_ring.Field_theory.condition, % 211.97/41.59 $_typeof_Coq.setoid_ring.Field_theory.denum, % 211.97/41.59 $_typeof_Coq.setoid_ring.Field_theory.linear, % 211.97/41.59 $_typeof_Coq.setoid_ring.Field_theory.mk_linear, % 211.97/41.59 $_typeof_Coq.setoid_ring.Field_theory.num, % 211.97/41.59 $_typeof_Coq.setoid_ring.Field_theory.rsplit, % 211.97/41.59 $_typeof_Coq.setoid_ring.Field_theory.rsplit_left, % 211.97/41.59 $_typeof_Coq.setoid_ring.Field_theory.rsplit_right, % 211.97/41.59 $_typeof_Coq.setoid_ring.InitialRing.Nopp, % 211.97/41.59 $_typeof_Coq.setoid_ring.InitialRing.Nsub, % 211.97/41.59 $_typeof_Coq.setoid_ring.InitialRing.gen_phiN, % 211.97/41.59 $_typeof_Coq.setoid_ring.InitialRing.gen_phiZ, % 211.97/41.59 $_typeof_Coq.setoid_ring.InitialRing.triv_div, % 211.97/41.59 $_typeof_Coq.setoid_ring.Ring.bool_eq, % 211.97/41.59 $_typeof_Coq.setoid_ring.Ring_polynom.Mon, % 211.97/41.59 $_typeof_Coq.setoid_ring.Ring_polynom.PEI, % 211.97/41.59 $_typeof_Coq.setoid_ring.Ring_polynom.PEO, % 211.97/41.59 $_typeof_Coq.setoid_ring.Ring_polynom.PEX, % 211.97/41.59 $_typeof_Coq.setoid_ring.Ring_polynom.PEadd, % 211.97/41.59 $_typeof_Coq.setoid_ring.Ring_polynom.PEc, % 211.97/41.59 $_typeof_Coq.setoid_ring.Ring_polynom.PEeval, % 211.97/41.59 $_typeof_Coq.setoid_ring.Ring_polynom.PEmul, % 211.97/41.59 $_typeof_Coq.setoid_ring.Ring_polynom.PEopp, % 211.97/41.59 $_typeof_Coq.setoid_ring.Ring_polynom.PEpow, % 211.97/41.59 $_typeof_Coq.setoid_ring.Ring_polynom.PEsub, % 211.97/41.59 $_typeof_Coq.setoid_ring.Ring_polynom.PExpr, % 211.97/41.59 $_typeof_Coq.setoid_ring.Ring_polynom.PX, % 211.97/41.59 $_typeof_Coq.setoid_ring.Ring_polynom.Pc, % 211.97/41.59 $_typeof_Coq.setoid_ring.Ring_polynom.Peq, % 211.97/41.59 $_typeof_Coq.setoid_ring.Ring_polynom.Pinj, % 211.97/41.59 $_typeof_Coq.setoid_ring.Ring_polynom.Pol, % 211.97/41.59 $_typeof_Coq.setoid_ring.Ring_tac.ring_subst_niter, % 211.97/41.59 $_typeof_Coq.setoid_ring.Ring_theory.Abstract, % 211.97/41.59 $_typeof_Coq.setoid_ring.Ring_theory.Computational, % 211.97/41.59 $_typeof_Coq.setoid_ring.Ring_theory.IDphi, % 211.97/41.59 $_typeof_Coq.setoid_ring.Ring_theory.Morphism, % 211.97/41.59 $_typeof_Coq.setoid_ring.Ring_theory.SRopp, % 211.97/41.59 $_typeof_Coq.setoid_ring.Ring_theory.SRsub, % 211.97/41.59 $_typeof_Coq.setoid_ring.Ring_theory.get_sign_None, % 211.97/41.59 $_typeof_Coq.setoid_ring.Ring_theory.id_phi_N, % 211.97/41.59 $_typeof_Coq.setoid_ring.Ring_theory.pow_N, % 211.97/41.59 $_typeof_Coq.setoid_ring.Ring_theory.pow_pos, % 211.97/41.59 $_typeof_Coq.setoid_ring.Ring_theory.ring_kind, % 211.97/41.59 $adef_$_case_Coq.Init.Datatypes.bool$102739_$a2, % 211.97/41.59 $adef_$_case_Coq.Init.Datatypes.bool$142229_$a4, % 211.97/41.59 $adef_$_case_Coq.Init.Datatypes.comparison$165612_$a5, % 211.97/41.59 $adef_$_case_Coq.Init.Datatypes.nat$21811_$a3, % 211.97/41.59 $adef_$_case_Coq.Init.Datatypes.nat$21833_$a1, % 211.97/41.59 $adef_$_case_Coq.Init.Datatypes.prod$8582_$a9, % 211.97/41.59 $adef_$_case_Coq.Numbers.BinNums.Z$21828_$a3, $adef_$_fix_20500_1_add_carry_$a2, % 211.97/41.59 $adef_$_lam_103102_$a1, $adef_$_lam_12266_$a1, $adef_$_lam_14771_$a2, % 211.97/41.59 $adef_$_lam_14771_$a4, $adef_$_lam_14779_$a2, $adef_$_lam_14779_$a4, % 211.97/41.59 $adef_$_lam_14787_$a2, $adef_$_lam_14787_$a4, $adef_$_lam_14795_$a2, % 211.97/41.59 $adef_$_lam_14795_$a4, $adef_$_let_var_6_p_21874_21877_$a4, % 211.97/41.59 $adef_$_let_var_6_p_21876_21878_$a4, $adef_$_prop_10581_$a3, % 211.97/41.59 $adef_$_prop_10582_$a3, $adef_$_prop_166330_$a2, $adef_$_prop_20885_$a2, % 211.97/41.59 $adef_$_prop_23380_$a4, $adef_$_prop_23381_$a3, $adef_$_prop_23382_$a3, % 211.97/41.59 $adef_$_prop_23383_$a3, $adef_$_prop_23384_$a3, $adef_$_prop_23385_$a3, % 211.97/41.59 $adef_$_prop_23386_$a2, $adef_$_prop_32246_$a2, $adef_$_prop_440_$a2, % 211.97/41.59 $adef_$_prop_441_$a2, $adef_Coq.Arith.Between.between_$a3, % 211.97/41.59 $adef_Coq.Arith.EqNat.eq_nat_$a2, $adef_Coq.Arith.Even.even_$a1, % 211.97/41.59 $adef_Coq.Arith.Even.odd_$a1, $adef_Coq.Arith.PeanoNat.Nat.b2n_$a1, % 211.97/41.59 $adef_Coq.Arith.PeanoNat.Nat.divide_$a2, $adef_Coq.Arith.PeanoNat.Nat.eqf_$a2, % 211.97/41.59 $adef_Coq.Bool.Bool.Is_true_$a1, $adef_Coq.Bool.Bool.ReflectF_$a1, % 211.97/41.59 $adef_Coq.Bool.Bool.ReflectT_$a1, $adef_Coq.Bool.Bool.eqb_$a2, % 211.97/41.59 $adef_Coq.Bool.Bool.reflect_$a2, $adef_Coq.Bool.Zerob.zerob_$a1, % 211.97/41.59 $adef_Coq.Classes.Morphisms.Proper_$a3, % 211.97/41.59 $adef_Coq.Classes.Morphisms.respectful_$a4, % 211.97/41.59 $adef_Coq.Classes.RelationClasses.Equivalence_$a2, % 211.97/41.59 $adef_Coq.Classes.RelationClasses.PreOrder_$a2, % 211.97/41.59 $adef_Coq.FSets.FSetPositive.PositiveSet.Equal_$a2, % 211.97/41.59 $adef_Coq.FSets.FSetPositive.PositiveSet.Exists_$a2, % 211.97/41.59 $adef_Coq.FSets.FSetPositive.PositiveSet.For_all_$a2, % 211.97/41.59 $adef_Coq.FSets.FSetPositive.PositiveSet.In_$a2, % 211.97/41.59 $adef_Coq.FSets.FSetPositive.PositiveSet.Node_$a3, % 211.97/41.59 $adef_Coq.FSets.FSetPositive.PositiveSet.Subset_$a2, % 211.97/41.59 $adef_Coq.FSets.FSetPositive.PositiveSet.equal_$a2, % 211.97/41.59 $adef_Coq.FSets.FSetPositive.PositiveSet.is_empty_$a1, % 211.97/41.59 $adef_Coq.FSets.FSetPositive.PositiveSet.mem_$a2, % 211.97/41.59 $adef_Coq.FSets.FSetPositive.PositiveSet.rev_append_$a2, % 211.97/41.59 $adef_Coq.Init.Datatypes.BoolSpec_$a3, $adef_Coq.Init.Datatypes.CompEqT_$a3, % 211.97/41.59 $adef_Coq.Init.Datatypes.CompGtT_$a3, $adef_Coq.Init.Datatypes.CompLtT_$a3, % 211.97/41.59 $adef_Coq.Init.Datatypes.CompOpp_$a1, $adef_Coq.Init.Datatypes.CompSpecT_$a5, % 211.97/41.59 $adef_Coq.Init.Datatypes.CompareSpecT_$a3, % 211.97/41.59 $adef_Coq.Init.Datatypes.CompareSpecT_$a4, % 211.97/41.59 $adef_Coq.Init.Datatypes.CompareSpec_$a4, $adef_Coq.Init.Datatypes.None_$a1, % 211.97/41.59 $adef_Coq.Init.Datatypes.S_$a1, $adef_Coq.Init.Datatypes.Some_$a2, % 211.97/41.59 $adef_Coq.Init.Datatypes.andb_$a2, $adef_Coq.Init.Datatypes.app_$a3, % 211.97/41.59 $adef_Coq.Init.Datatypes.cons_$a3, $adef_Coq.Init.Datatypes.fst_$a3, % 211.97/41.59 $adef_Coq.Init.Datatypes.inl_$a3, $adef_Coq.Init.Datatypes.inr_$a3, % 211.97/41.59 $adef_Coq.Init.Datatypes.length_$a2, $adef_Coq.Init.Datatypes.list_$a1, % 211.97/41.59 $adef_Coq.Init.Datatypes.nat_rect_$a3, $adef_Coq.Init.Datatypes.negb_$a1, % 211.97/41.59 $adef_Coq.Init.Datatypes.nil_$a1, $adef_Coq.Init.Datatypes.option_$a1, % 211.97/41.59 $adef_Coq.Init.Datatypes.orb_$a2, $adef_Coq.Init.Datatypes.pair_$a4, % 211.97/41.59 $adef_Coq.Init.Datatypes.prod_$a2, $adef_Coq.Init.Datatypes.snd_$a3, % 211.97/41.59 $adef_Coq.Init.Datatypes.sum_$a2, $adef_Coq.Init.Datatypes.xorb_$a2, % 211.97/41.59 $adef_Coq.Init.Logic.eq_rect_$a5, $adef_Coq.Init.Logic.eq_refl_$a2, % 211.97/41.59 $adef_Coq.Init.Nat.add_$a2, $adef_Coq.Init.Nat.compare_$a2, % 211.97/41.59 $adef_Coq.Init.Nat.div2_$a1, $adef_Coq.Init.Nat.div_$a2, % 211.97/41.59 $adef_Coq.Init.Nat.divmod_$a4, $adef_Coq.Init.Nat.double_$a1, % 211.97/41.59 $adef_Coq.Init.Nat.eqb_$a2, $adef_Coq.Init.Nat.even_$a1, % 211.97/41.59 $adef_Coq.Init.Nat.gcd_$a2, $adef_Coq.Init.Nat.max_$a2, % 211.97/41.59 $adef_Coq.Init.Nat.min_$a2, $adef_Coq.Init.Nat.modulo_$a2, % 211.97/41.59 $adef_Coq.Init.Nat.mul_$a2, $adef_Coq.Init.Nat.odd_$a1, % 211.97/41.59 $adef_Coq.Init.Nat.pow_$a2, $adef_Coq.Init.Nat.pred_$a1, % 211.97/41.59 $adef_Coq.Init.Nat.shiftl_$a1, $adef_Coq.Init.Nat.sqrt_$a1, % 211.97/41.59 $adef_Coq.Init.Nat.sqrt_iter_$a4, $adef_Coq.Init.Nat.sub_$a2, % 211.97/41.59 $adef_Coq.Init.Nat.testbit_$a2, $adef_Coq.Init.Peano.gt_$a2, % 211.97/41.59 $adef_Coq.Init.Peano.le_$a2, $adef_Coq.Init.Peano.lt_$a2, % 211.97/41.59 $adef_Coq.Init.Specif.exist2_$a4, $adef_Coq.Init.Specif.existT2_$a6, % 211.97/41.59 $adef_Coq.Init.Specif.existT_$a4, $adef_Coq.Init.Specif.exist_$a3, % 211.97/41.59 $adef_Coq.Init.Specif.inleft_$a3, $adef_Coq.Init.Specif.inright_$a2, % 211.97/41.59 $adef_Coq.Init.Specif.left_$a2, $adef_Coq.Init.Specif.proj1_sig_$a3, % 211.97/41.59 $adef_Coq.Init.Specif.projT1_$a3, $adef_Coq.Init.Specif.projT2_$a3, % 211.97/41.59 $adef_Coq.Init.Specif.right_$a2, $adef_Coq.Init.Specif.sig2_$a3, % 211.97/41.59 $adef_Coq.Init.Specif.sigT2_$a3, $adef_Coq.Init.Specif.sigT_$a2, % 211.97/41.59 $adef_Coq.Init.Specif.sig_$a2, $adef_Coq.Init.Specif.sumbool_$a2, % 211.97/41.59 $adef_Coq.Init.Specif.sumor_$a2, $adef_Coq.Init.Wf.Acc_$a3, % 211.97/41.59 $adef_Coq.Init.Wf.well_founded_$a2, $adef_Coq.Lists.List.Forall_$a3, % 211.97/41.59 $adef_Coq.Lists.List.In_$a3, $adef_Coq.Lists.List.NoDup_$a2, % 211.97/41.59 $adef_Coq.Lists.List.fold_left_$a5, $adef_Coq.Lists.List.fold_right_$a5, % 211.97/41.59 $adef_Coq.Lists.List.last_$a3, $adef_Coq.Lists.List.map_$a4, % 211.97/41.59 $adef_Coq.Lists.List.nth_$a4, $adef_Coq.Lists.SetoidList.InA_$a4, % 211.97/41.59 $adef_Coq.Lists.SetoidList.NoDupA_$a3, % 211.97/41.59 $adef_Coq.Lists.SetoidList.compat_bool_$a3, % 211.97/41.59 $adef_Coq.Lists.SetoidList.compat_op_$a5, % 211.97/41.59 $adef_Coq.Lists.SetoidList.transpose_$a4, % 211.97/41.59 $adef_Coq.Logic.Decidable.decidable_$a1, % 211.97/41.59 $adef_Coq.Logic.EqdepFacts.Eq_dep_eq_on_$a4, % 211.97/41.59 $adef_Coq.Logic.EqdepFacts.Eq_rect_eq_$a1, % 211.97/41.59 $adef_Coq.Logic.EqdepFacts.Eq_rect_eq_on_$a4, % 211.97/41.59 $adef_Coq.Logic.EqdepFacts.Streicher_K_on__$a3, % 211.97/41.59 $adef_Coq.Logic.EqdepFacts.UIP__$a1, $adef_Coq.Logic.EqdepFacts.UIP_on__$a3, % 211.97/41.59 $adef_Coq.Logic.EqdepFacts.UIP_refl_on__$a1, % 211.97/41.59 $adef_Coq.Logic.EqdepFacts.UIP_refl_on__$a2, % 211.97/41.59 $adef_Coq.Logic.EqdepFacts.eq_dep1_$a6, $adef_Coq.Logic.EqdepFacts.eq_dep_$a6, % 211.97/41.59 $adef_Coq.NArith.BinNat.N.b2n_$a1, $adef_Coq.NArith.BinNat.N.divide_$a2, % 211.97/41.59 $adef_Coq.NArith.BinNat.N.eqf_$a2, $adef_Coq.NArith.BinNat.N.le_$a2, % 211.97/41.59 $adef_Coq.NArith.BinNat.N.lt_$a2, $adef_Coq.NArith.BinNatDef.N.add_$a2, % 211.97/41.59 $adef_Coq.NArith.BinNatDef.N.compare_$a2, $adef_Coq.NArith.BinNatDef.N.div2_$a1, % 211.97/41.59 $adef_Coq.NArith.BinNatDef.N.div_$a2, $adef_Coq.NArith.BinNatDef.N.div_eucl_$a2, % 211.97/41.59 $adef_Coq.NArith.BinNatDef.N.double_$a1, $adef_Coq.NArith.BinNatDef.N.eqb_$a2, % 211.97/41.59 $adef_Coq.NArith.BinNatDef.N.even_$a1, $adef_Coq.NArith.BinNatDef.N.gcd_$a2, % 211.97/41.59 $adef_Coq.NArith.BinNatDef.N.log2_$a1, $adef_Coq.NArith.BinNatDef.N.max_$a2, % 211.97/41.59 $adef_Coq.NArith.BinNatDef.N.min_$a2, $adef_Coq.NArith.BinNatDef.N.modulo_$a2, % 211.97/41.59 $adef_Coq.NArith.BinNatDef.N.mul_$a2, $adef_Coq.NArith.BinNatDef.N.odd_$a1, % 211.97/41.59 $adef_Coq.NArith.BinNatDef.N.pow_$a2, $adef_Coq.NArith.BinNatDef.N.pred_$a1, % 211.97/41.59 $adef_Coq.NArith.BinNatDef.N.sqrt_$a1, $adef_Coq.NArith.BinNatDef.N.sub_$a2, % 211.97/41.59 $adef_Coq.NArith.BinNatDef.N.succ_$a1, % 211.97/41.59 $adef_Coq.NArith.BinNatDef.N.succ_double_$a1, % 211.97/41.59 $adef_Coq.NArith.BinNatDef.N.testbit_$a2, % 211.97/41.59 $adef_Coq.NArith.BinNatDef.N.to_nat_$a1, $adef_Coq.Numbers.BinNums.Npos_$a1, % 211.97/41.59 $adef_Coq.Numbers.BinNums.Zneg_$a1, $adef_Coq.Numbers.BinNums.Zpos_$a1, % 211.97/41.59 $adef_Coq.Numbers.BinNums.xI_$a1, $adef_Coq.Numbers.BinNums.xO_$a1, % 211.97/41.59 $adef_Coq.PArith.BinPos.Pos.SqrtSpec_$a2, % 211.97/41.59 $adef_Coq.PArith.BinPos.Pos.SubMaskSpec_$a3, $adef_Coq.PArith.BinPos.Pos.le_$a2, % 211.97/41.59 $adef_Coq.PArith.BinPos.Pos.lt_$a2, $adef_Coq.PArith.BinPos.Pos.switch_Eq_$a2, % 211.97/41.59 $adef_Coq.PArith.BinPosDef.Pos.IsPos_$a1, % 211.97/41.59 $adef_Coq.PArith.BinPosDef.Pos.add_$a2, % 211.97/41.59 $adef_Coq.PArith.BinPosDef.Pos.compare_$a2, % 211.97/41.59 $adef_Coq.PArith.BinPosDef.Pos.compare_cont_$a1, % 211.97/41.59 $adef_Coq.PArith.BinPosDef.Pos.eqb_$a2, $adef_Coq.PArith.BinPosDef.Pos.gcd_$a2, % 211.97/41.59 $adef_Coq.PArith.BinPosDef.Pos.iter_$a4, % 211.97/41.59 $adef_Coq.PArith.BinPosDef.Pos.iter_op_$a4, % 211.97/41.59 $adef_Coq.PArith.BinPosDef.Pos.max_$a2, $adef_Coq.PArith.BinPosDef.Pos.min_$a2, % 211.97/41.59 $adef_Coq.PArith.BinPosDef.Pos.mul_$a2, % 211.97/41.59 $adef_Coq.PArith.BinPosDef.Pos.of_nat_$a1, % 211.97/41.59 $adef_Coq.PArith.BinPosDef.Pos.of_succ_nat_$a1, % 211.97/41.59 $adef_Coq.PArith.BinPosDef.Pos.pow_$a2, $adef_Coq.PArith.BinPosDef.Pos.pred_$a1, % 211.97/41.59 $adef_Coq.PArith.BinPosDef.Pos.pred_N_$a1, % 211.97/41.59 $adef_Coq.PArith.BinPosDef.Pos.pred_double_$a1, % 211.97/41.59 $adef_Coq.PArith.BinPosDef.Pos.size_$a1, % 211.97/41.59 $adef_Coq.PArith.BinPosDef.Pos.sqrt_$a1, $adef_Coq.PArith.BinPosDef.Pos.sub_$a2, % 211.97/41.59 $adef_Coq.PArith.BinPosDef.Pos.sub_mask_$a2, % 211.97/41.59 $adef_Coq.PArith.BinPosDef.Pos.succ_$a1, % 211.97/41.59 $adef_Coq.PArith.BinPosDef.Pos.testbit_$a2, % 211.97/41.59 $adef_Coq.PArith.BinPosDef.Pos.to_nat_$a1, % 211.97/41.59 $adef_Coq.QArith.QArith_base.Qden_$a1, $adef_Coq.QArith.QArith_base.Qmake_$a2, % 211.97/41.59 $adef_Coq.QArith.QArith_base.Qnum_$a1, $adef_Coq.Reals.RIneq.Rsqr_$a1, % 211.97/41.59 $adef_Coq.Reals.RIneq.mknonzeroreal_$a1, $adef_Coq.Reals.Rdefinitions.IPR_$a1, % 211.97/41.59 $adef_Coq.Reals.Rdefinitions.IZR_$a1, $adef_Coq.Reals.Rdefinitions.Rdiv_$a2, % 211.97/41.59 $adef_Coq.Reals.Rdefinitions.Rge_$a2, $adef_Coq.Reals.Rdefinitions.Rgt_$a2, % 211.97/41.59 $adef_Coq.Reals.Rdefinitions.Rinv_$a1, $adef_Coq.Reals.Rdefinitions.Rle_$a2, % 211.97/41.59 $adef_Coq.Reals.Rdefinitions.Rlt_$a2, $adef_Coq.Reals.Rdefinitions.Rminus_$a2, % 211.97/41.59 $adef_Coq.Reals.Rdefinitions.Rmult_$a2, $adef_Coq.Reals.Rdefinitions.Ropp_$a1, % 211.97/41.59 $adef_Coq.Reals.Rdefinitions.Rplus_$a2, $adef_Coq.Reals.Rfunctions.Z_spec_$a2, % 211.97/41.59 $adef_Coq.Reals.Rfunctions.ZintNeg_$a2, $adef_Coq.Reals.Rfunctions.ZintNull_$a1, % 211.97/41.59 $adef_Coq.Reals.Rfunctions.ZintPos_$a2, $adef_Coq.Reals.Rpow_def.pow_$a2, % 211.97/41.59 $adef_Coq.Relations.Relation_Definitions.relation_$a1, % 211.97/41.59 $adef_Coq.Setoids.Setoid.Setoid_Theory_$a2, % 211.97/41.59 $adef_Coq.Sorting.Sorted.StronglySorted_$a3, $adef_Coq.Strings.Ascii.Ascii_$a8, % 211.97/41.59 $adef_Coq.Strings.Ascii.nat_of_ascii_$a1, $adef_Coq.Strings.String.String_$a2, % 211.97/41.59 $adef_Coq.Structures.OrderedType.Compare_$a5, % 211.97/41.59 $adef_Coq.Structures.OrderedType.EQ_$a5, % 211.97/41.59 $adef_Coq.Structures.OrderedType.GT_$a5, % 211.97/41.59 $adef_Coq.Structures.OrderedType.LT_$a5, % 211.97/41.59 $adef_Coq.Structures.OrderedTypeEx.String_as_OT.lts_$a2, % 211.97/41.59 $adef_Coq.Structures.OrderedTypeEx.Z_as_OT.lt_$a2, $adef_Coq.Vectors.Fin.F1_$a1, % 211.97/41.59 $adef_Coq.Vectors.Fin.FS_$a2, $adef_Coq.Vectors.Fin.t_$a1, % 211.97/41.59 $adef_Coq.Vectors.VectorDef.cons_$a4, % 211.97/41.59 $adef_Coq.Vectors.VectorDef.fold_right_$a6, $adef_Coq.Vectors.VectorDef.nil_$a1, % 211.97/41.59 $adef_Coq.Vectors.VectorDef.t_$a2, $adef_Coq.ZArith.BinInt.Z.Bezout_$a3, % 211.97/41.59 $adef_Coq.ZArith.BinInt.Z.b2z_$a1, $adef_Coq.ZArith.BinInt.Z.divide_$a2, % 211.97/41.59 $adef_Coq.ZArith.BinInt.Z.eqf_$a2, $adef_Coq.ZArith.BinInt.Z.ge_$a2, % 211.97/41.59 $adef_Coq.ZArith.BinInt.Z.gt_$a2, $adef_Coq.ZArith.BinInt.Z.le_$a2, % 211.97/41.59 $adef_Coq.ZArith.BinInt.Z.lt_$a2, $adef_Coq.ZArith.BinInt.Zne_$a2, % 211.97/41.59 $adef_Coq.ZArith.BinIntDef.Z.abs_$a1, $adef_Coq.ZArith.BinIntDef.Z.add_$a2, % 211.97/41.59 $adef_Coq.ZArith.BinIntDef.Z.compare_$a2, $adef_Coq.ZArith.BinIntDef.Z.div_$a2, % 211.97/41.59 $adef_Coq.ZArith.BinIntDef.Z.div_eucl_$a2, $adef_Coq.ZArith.BinIntDef.Z.eqb_$a2, % 211.97/41.59 $adef_Coq.ZArith.BinIntDef.Z.gcd_$a2, $adef_Coq.ZArith.BinIntDef.Z.leb_$a2, % 211.97/41.59 $adef_Coq.ZArith.BinIntDef.Z.log2_$a1, $adef_Coq.ZArith.BinIntDef.Z.max_$a2, % 211.97/41.59 $adef_Coq.ZArith.BinIntDef.Z.min_$a2, $adef_Coq.ZArith.BinIntDef.Z.modulo_$a2, % 211.97/41.59 $adef_Coq.ZArith.BinIntDef.Z.mul_$a2, $adef_Coq.ZArith.BinIntDef.Z.of_N_$a1, % 211.97/41.59 $adef_Coq.ZArith.BinIntDef.Z.of_nat_$a1, $adef_Coq.ZArith.BinIntDef.Z.opp_$a1, % 211.97/41.59 $adef_Coq.ZArith.BinIntDef.Z.pos_sub_$a2, $adef_Coq.ZArith.BinIntDef.Z.pow_$a2, % 211.97/41.59 $adef_Coq.ZArith.BinIntDef.Z.pow_pos_$a2, $adef_Coq.ZArith.BinIntDef.Z.pred_$a1, % 211.97/41.59 $adef_Coq.ZArith.BinIntDef.Z.quot_$a2, $adef_Coq.ZArith.BinIntDef.Z.quotrem_$a2, % 211.97/41.59 $adef_Coq.ZArith.BinIntDef.Z.rem_$a2, $adef_Coq.ZArith.BinIntDef.Z.sgn_$a1, % 211.97/41.59 $adef_Coq.ZArith.BinIntDef.Z.sqrt_$a1, $adef_Coq.ZArith.BinIntDef.Z.sub_$a2, % 211.97/41.59 $adef_Coq.ZArith.BinIntDef.Z.succ_$a1, $adef_Coq.ZArith.BinIntDef.Z.to_pos_$a1, % 211.97/41.59 $adef_Coq.ZArith.Zbool.Zeq_bool_$a2, $adef_Coq.ZArith.Zdiv.Remainder_$a2, % 211.97/41.59 $adef_Coq.ZArith.Znumtheory.Bezout_$a3, $adef_Coq.ZArith.Znumtheory.Euclid_$a2, % 211.97/41.59 $adef_Coq.ZArith.Znumtheory.Euclid_intro_$a5, % 211.97/41.59 $adef_Coq.ZArith.Znumtheory.Zis_gcd_$a3, % 211.97/41.59 $adef_Coq.ZArith.Zpower.Zdiv_rest_proof_$a4, % 211.97/41.59 $adef_Coq.ZArith.Zpower.Zdiv_rest_proofs_$a2, % 211.97/41.59 $adef_Coq.ZArith.Zpower.two_power_pos_$a1, $adef_Coq.micromega.Env.Env_$a1, % 211.97/41.59 $adef_Coq.micromega.Env.jump_$a4, $adef_Coq.micromega.Env.nth_$a3, % 211.97/41.59 $adef_Coq.micromega.EnvRing.Mphi_$a5, $adef_Coq.micromega.EnvRing.PEX_$a2, % 211.97/41.59 $adef_Coq.micromega.EnvRing.PEadd_$a3, $adef_Coq.micromega.EnvRing.PEc_$a2, % 211.97/41.59 $adef_Coq.micromega.EnvRing.PEmul_$a3, $adef_Coq.micromega.EnvRing.PEopp_$a2, % 211.97/41.59 $adef_Coq.micromega.EnvRing.PEpow_$a3, $adef_Coq.micromega.EnvRing.PEsub_$a3, % 211.97/41.59 $adef_Coq.micromega.EnvRing.PExpr_$a1, $adef_Coq.micromega.EnvRing.PX_$a4, % 211.97/41.59 $adef_Coq.micromega.EnvRing.Pc_$a2, $adef_Coq.micromega.EnvRing.Pinj_$a3, % 211.97/41.59 $adef_Coq.micromega.EnvRing.Pol_$a1, $adef_Coq.micromega.EnvRing.Pphi_$a7, % 211.97/41.59 $adef_Coq.micromega.EnvRing.vmon_$a2, $adef_Coq.micromega.EnvRing.zmon_$a2, % 211.97/41.59 $adef_Coq.micromega.OrderedRing.SOR_$a10, % 211.97/41.59 $adef_Coq.micromega.Refl.make_conj_$a3, $adef_Coq.micromega.Refl.make_impl_$a4, % 211.97/41.59 $adef_Coq.micromega.RingMicromega.Build_Formula_$a4, % 211.97/41.59 $adef_Coq.micromega.RingMicromega.Formula_$a1, % 211.97/41.59 $adef_Coq.micromega.RingMicromega.PolEnv_$a1, % 211.97/41.59 $adef_Coq.micromega.RingMicromega.SORaddon_$a22, % 211.97/41.59 $adef_Coq.micromega.RingMicromega.eval_op2_$a5, $adef_Coq.micromega.Tauto.A_$a6, % 211.97/41.59 $adef_Coq.micromega.Tauto.Cj_$a6, $adef_Coq.micromega.Tauto.D_$a6, % 211.97/41.59 $adef_Coq.micromega.Tauto.FF_$a4, $adef_Coq.micromega.Tauto.GFormula_$a4, % 211.97/41.59 $adef_Coq.micromega.Tauto.I_$a7, $adef_Coq.micromega.Tauto.N_$a5, % 211.97/41.59 $adef_Coq.micromega.Tauto.TT_$a4, $adef_Coq.micromega.Tauto.X_$a5, % 211.97/41.59 $adef_Coq.micromega.ZMicromega.Vars.Facts.MP.Dec.FSetDecideAuxiliary.FSet_elt_Prop_$a1, % 211.97/41.59 $adef_Coq.micromega.ZMicromega.is_diff_env_elt_$a4, % 211.97/41.59 $adef_Coq.setoid_ring.BinList.nth_$a4, % 211.97/41.59 $adef_Coq.setoid_ring.Field_theory.FEI_$a1, % 211.97/41.59 $adef_Coq.setoid_ring.Field_theory.FEO_$a1, % 211.97/41.59 $adef_Coq.setoid_ring.Field_theory.FEX_$a2, % 211.97/41.59 $adef_Coq.setoid_ring.Field_theory.FEadd_$a3, % 211.97/41.59 $adef_Coq.setoid_ring.Field_theory.FEc_$a2, % 211.97/41.59 $adef_Coq.setoid_ring.Field_theory.FEdiv_$a3, % 211.97/41.59 $adef_Coq.setoid_ring.Field_theory.FEinv_$a2, % 211.97/41.59 $adef_Coq.setoid_ring.Field_theory.FEmul_$a3, % 211.97/41.59 $adef_Coq.setoid_ring.Field_theory.FEopp_$a2, % 211.97/41.59 $adef_Coq.setoid_ring.Field_theory.FEpow_$a3, % 211.97/41.59 $adef_Coq.setoid_ring.Field_theory.FEsub_$a3, % 211.97/41.59 $adef_Coq.setoid_ring.Field_theory.FExpr_$a1, % 211.97/41.59 $adef_Coq.setoid_ring.Field_theory.Fapp_$a4, % 211.97/41.59 $adef_Coq.setoid_ring.Field_theory.almost_field_theory_$a10, % 211.97/41.59 $adef_Coq.setoid_ring.Field_theory.condition_$a2, % 211.97/41.59 $adef_Coq.setoid_ring.Field_theory.denum_$a2, % 211.97/41.59 $adef_Coq.setoid_ring.Field_theory.linear_$a1, % 211.97/41.59 $adef_Coq.setoid_ring.Field_theory.mk_linear_$a4, % 211.97/41.59 $adef_Coq.setoid_ring.Field_theory.mk_rsplit_$a4, % 211.97/41.59 $adef_Coq.setoid_ring.Field_theory.num_$a2, % 211.97/41.59 $adef_Coq.setoid_ring.Field_theory.rsplit_$a1, % 211.97/41.59 $adef_Coq.setoid_ring.Field_theory.rsplit_left_$a2, % 211.97/41.59 $adef_Coq.setoid_ring.Field_theory.rsplit_right_$a2, % 211.97/41.59 $adef_Coq.setoid_ring.InitialRing.gen_phiN_$a6, % 211.97/41.59 $adef_Coq.setoid_ring.InitialRing.gen_phiPOS_$a5, % 211.97/41.59 $adef_Coq.setoid_ring.InitialRing.gen_phiZ_$a7, % 211.97/41.59 $adef_Coq.setoid_ring.InitialRing.triv_div_$a6, % 211.97/41.59 $adef_Coq.setoid_ring.Ring.bool_eq_$a2, % 211.97/41.59 $adef_Coq.setoid_ring.Ring_polynom.PEI_$a1, % 211.97/41.59 $adef_Coq.setoid_ring.Ring_polynom.PEO_$a1, % 211.97/41.59 $adef_Coq.setoid_ring.Ring_polynom.PEX_$a2, % 211.97/41.59 $adef_Coq.setoid_ring.Ring_polynom.PEadd_$a3, % 211.97/41.59 $adef_Coq.setoid_ring.Ring_polynom.PEc_$a2, % 211.97/41.59 $adef_Coq.setoid_ring.Ring_polynom.PEeval_$a14, % 211.97/41.59 $adef_Coq.setoid_ring.Ring_polynom.PEmul_$a3, % 211.97/41.59 $adef_Coq.setoid_ring.Ring_polynom.PEopp_$a2, % 211.97/41.59 $adef_Coq.setoid_ring.Ring_polynom.PEpow_$a3, % 211.97/41.59 $adef_Coq.setoid_ring.Ring_polynom.PEsub_$a3, % 211.97/41.59 $adef_Coq.setoid_ring.Ring_polynom.PExpr_$a1, % 211.97/41.59 $adef_Coq.setoid_ring.Ring_polynom.PX_$a4, % 211.97/41.59 $adef_Coq.setoid_ring.Ring_polynom.Pc_$a2, % 211.97/41.59 $adef_Coq.setoid_ring.Ring_polynom.Peq_$a4, % 211.97/41.59 $adef_Coq.setoid_ring.Ring_polynom.Pinj_$a3, % 211.97/41.59 $adef_Coq.setoid_ring.Ring_polynom.Pol_$a1, % 211.97/41.59 $adef_Coq.setoid_ring.Ring_polynom.vmon_$a2, % 211.97/41.59 $adef_Coq.setoid_ring.Ring_polynom.zmon_$a2, % 211.97/41.59 $adef_Coq.setoid_ring.Ring_theory.Computational_$a3, % 211.97/41.59 $adef_Coq.setoid_ring.Ring_theory.IDphi_$a2, % 211.97/41.59 $adef_Coq.setoid_ring.Ring_theory.Morphism_$a17, % 211.97/41.59 $adef_Coq.setoid_ring.Ring_theory.SRopp_$a1, % 211.97/41.59 $adef_Coq.setoid_ring.Ring_theory.SRopp_$a2, % 211.97/41.59 $adef_Coq.setoid_ring.Ring_theory.SRsub_$a2, % 211.97/41.59 $adef_Coq.setoid_ring.Ring_theory.SRsub_$a4, % 211.97/41.59 $adef_Coq.setoid_ring.Ring_theory.almost_ring_theory_$a8, % 211.97/41.59 $adef_Coq.setoid_ring.Ring_theory.div_theory_$a7, % 211.97/41.59 $adef_Coq.setoid_ring.Ring_theory.get_sign_None_$a2, % 211.97/41.59 $adef_Coq.setoid_ring.Ring_theory.id_phi_N_$a1, % 211.97/41.59 $adef_Coq.setoid_ring.Ring_theory.pow_N_$a5, % 211.97/41.59 $adef_Coq.setoid_ring.Ring_theory.pow_pos_$a4, % 211.97/41.59 $adef_Coq.setoid_ring.Ring_theory.power_theory_$a7, % 211.97/41.59 $adef_Coq.setoid_ring.Ring_theory.ring_eq_ext_$a5, % 211.97/41.59 $adef_Coq.setoid_ring.Ring_theory.ring_morph_$a17, % 211.97/41.59 $adef_Coq.setoid_ring.Ring_theory.ring_theory_$a8, % 211.97/41.59 $adef_Coq.setoid_ring.Ring_theory.semi_morph_$a13, % 211.97/41.59 $adef_Coq.setoid_ring.Ring_theory.sign_theory_$a4, % 211.97/41.59 $adef_Coq.setoid_ring.Ring_theory.sring_eq_ext_$a4, $tdef_$_type_10047, % 211.97/41.59 $tdef_$_type_10051, $tdef_$_type_10055, $tdef_$_type_10101, $tdef_$_type_10113, % 211.97/41.59 $tdef_$_type_10125, $tdef_$_type_10127, $tdef_$_type_10132, $tdef_$_type_101786, % 211.97/41.59 $tdef_$_type_10187, $tdef_$_type_10200, $tdef_$_type_10202, $tdef_$_type_1022, % 211.97/41.59 $tdef_$_type_10221, $tdef_$_type_102742, $tdef_$_type_102836, % 211.97/41.59 $tdef_$_type_103177, $tdef_$_type_103179, $tdef_$_type_10574, % 211.97/41.59 $tdef_$_type_10579, $tdef_$_type_10585, $tdef_$_type_1104, $tdef_$_type_11789, % 211.97/41.59 $tdef_$_type_11847, $tdef_$_type_11910, $tdef_$_type_1197, $tdef_$_type_12041, % 211.97/41.59 $tdef_$_type_12066, $tdef_$_type_12105, $tdef_$_type_12109, $tdef_$_type_12123, % 211.97/41.59 $tdef_$_type_12222, $tdef_$_type_12237, $tdef_$_type_12251, $tdef_$_type_12719, % 211.97/41.59 $tdef_$_type_1279, $tdef_$_type_12820, $tdef_$_type_12921, $tdef_$_type_13011, % 211.97/41.59 $tdef_$_type_13112, $tdef_$_type_13213, $tdef_$_type_13314, $tdef_$_type_13480, % 211.97/41.59 $tdef_$_type_13499, $tdef_$_type_13519, $tdef_$_type_13622, $tdef_$_type_13632, % 211.97/41.59 $tdef_$_type_13638, $tdef_$_type_13651, $tdef_$_type_13656, $tdef_$_type_13667, % 211.97/41.59 $tdef_$_type_1372, $tdef_$_type_1381, $tdef_$_type_13833, $tdef_$_type_13882, % 211.97/41.59 $tdef_$_type_1390, $tdef_$_type_141300, $tdef_$_type_145287, % 211.97/41.59 $tdef_$_type_145293, $tdef_$_type_14832, $tdef_$_type_15251, $tdef_$_type_15259, % 211.97/41.59 $tdef_$_type_15262, $tdef_$_type_15391, $tdef_$_type_154381, % 211.97/41.59 $tdef_$_type_154397, $tdef_$_type_154763, $tdef_$_type_155143, % 211.97/41.59 $tdef_$_type_156168, $tdef_$_type_156173, $tdef_$_type_158368, % 211.97/41.59 $tdef_$_type_158399, $tdef_$_type_159221, $tdef_$_type_159569, $tdef_$_type_16, % 211.97/41.59 $tdef_$_type_16600, $tdef_$_type_16603, $tdef_$_type_16606, $tdef_$_type_166265, % 211.97/41.59 $tdef_$_type_166277, $tdef_$_type_166286, $tdef_$_type_166294, % 211.97/41.59 $tdef_$_type_166299, $tdef_$_type_166308, $tdef_$_type_166313, % 211.97/41.59 $tdef_$_type_166325, $tdef_$_type_166378, $tdef_$_type_166386, % 211.97/41.59 $tdef_$_type_166389, $tdef_$_type_16640, $tdef_$_type_166723, % 211.97/41.59 $tdef_$_type_16731, $tdef_$_type_16754, $tdef_$_type_16777, $tdef_$_type_16800, % 211.97/41.59 $tdef_$_type_16818, $tdef_$_type_16844, $tdef_$_type_16862, $tdef_$_type_17120, % 211.97/41.59 $tdef_$_type_17245, $tdef_$_type_17370, $tdef_$_type_17495, $tdef_$_type_17620, % 211.97/41.59 $tdef_$_type_17745, $tdef_$_type_17856, $tdef_$_type_17892, $tdef_$_type_17903, % 211.97/41.59 $tdef_$_type_17934, $tdef_$_type_17946, $tdef_$_type_17988, $tdef_$_type_18023, % 211.97/41.59 $tdef_$_type_18034, $tdef_$_type_18054, $tdef_$_type_18058, $tdef_$_type_18076, % 211.97/41.59 $tdef_$_type_18093, $tdef_$_type_18097, $tdef_$_type_18100, $tdef_$_type_18117, % 211.97/41.59 $tdef_$_type_183, $tdef_$_type_18407, $tdef_$_type_20068, $tdef_$_type_20144, % 211.97/41.59 $tdef_$_type_20153, $tdef_$_type_20164, $tdef_$_type_20269, $tdef_$_type_20462, % 211.97/41.59 $tdef_$_type_20466, $tdef_$_type_20530, $tdef_$_type_20574, $tdef_$_type_20742, % 211.97/41.59 $tdef_$_type_2076, $tdef_$_type_2081, $tdef_$_type_20841, $tdef_$_type_2090, % 211.97/41.59 $tdef_$_type_20994, $tdef_$_type_21039, $tdef_$_type_2115, $tdef_$_type_2135, % 211.97/41.59 $tdef_$_type_22, $tdef_$_type_22657, $tdef_$_type_22667, $tdef_$_type_22693, % 211.97/41.59 $tdef_$_type_22701, $tdef_$_type_22709, $tdef_$_type_22749, $tdef_$_type_22757, % 211.97/41.59 $tdef_$_type_22765, $tdef_$_type_22791, $tdef_$_type_22874, $tdef_$_type_23298, % 211.97/41.59 $tdef_$_type_23408, $tdef_$_type_23504, $tdef_$_type_23614, $tdef_$_type_23691, % 211.97/41.59 $tdef_$_type_23696, $tdef_$_type_23727, $tdef_$_type_24, $tdef_$_type_2404, % 211.97/41.59 $tdef_$_type_24262, $tdef_$_type_24608, $tdef_$_type_2469, $tdef_$_type_2493, % 211.97/41.59 $tdef_$_type_24954, $tdef_$_type_2507, $tdef_$_type_2514, $tdef_$_type_25277, % 211.97/41.59 $tdef_$_type_25623, $tdef_$_type_25969, $tdef_$_type_26315, $tdef_$_type_26661, % 211.97/41.59 $tdef_$_type_27007, $tdef_$_type_27330, $tdef_$_type_27676, $tdef_$_type_28022, % 211.97/41.59 $tdef_$_type_28345, $tdef_$_type_28668, $tdef_$_type_29014, $tdef_$_type_2931, % 211.97/41.59 $tdef_$_type_29362, $tdef_$_type_29371, $tdef_$_type_29419, $tdef_$_type_29456, % 211.97/41.59 $tdef_$_type_29472, $tdef_$_type_29568, $tdef_$_type_29571, $tdef_$_type_29693, % 211.97/41.59 $tdef_$_type_29696, $tdef_$_type_29701, $tdef_$_type_29709, $tdef_$_type_29712, % 211.97/41.59 $tdef_$_type_29725, $tdef_$_type_29734, $tdef_$_type_29739, $tdef_$_type_29742, % 211.97/41.59 $tdef_$_type_29747, $tdef_$_type_29750, $tdef_$_type_29833, $tdef_$_type_29857, % 211.97/41.59 $tdef_$_type_29886, $tdef_$_type_29893, $tdef_$_type_29957, $tdef_$_type_30063, % 211.97/41.59 $tdef_$_type_30078, $tdef_$_type_301, $tdef_$_type_30661, $tdef_$_type_30688, % 211.97/41.59 $tdef_$_type_307, $tdef_$_type_30714, $tdef_$_type_31241, $tdef_$_type_31363, % 211.97/41.59 $tdef_$_type_31374, $tdef_$_type_31633, $tdef_$_type_31798, $tdef_$_type_31818, % 211.97/41.59 $tdef_$_type_31840, $tdef_$_type_31858, $tdef_$_type_31864, $tdef_$_type_31881, % 211.97/41.59 $tdef_$_type_31887, $tdef_$_type_31893, $tdef_$_type_31898, $tdef_$_type_31901, % 211.97/41.59 $tdef_$_type_31952, $tdef_$_type_322, $tdef_$_type_32239, $tdef_$_type_32250, % 211.97/41.59 $tdef_$_type_3227, $tdef_$_type_32317, $tdef_$_type_32357, $tdef_$_type_32412, % 211.97/41.59 $tdef_$_type_32438, $tdef_$_type_32443, $tdef_$_type_32451, $tdef_$_type_32468, % 211.97/41.59 $tdef_$_type_32472, $tdef_$_type_3420, $tdef_$_type_355, $tdef_$_type_364, % 211.97/41.59 $tdef_$_type_367, $tdef_$_type_373, $tdef_$_type_386, $tdef_$_type_393, % 211.97/41.59 $tdef_$_type_397, $tdef_$_type_4, $tdef_$_type_400, $tdef_$_type_405, % 211.97/41.59 $tdef_$_type_417, $tdef_$_type_438, $tdef_$_type_4596, $tdef_$_type_462, % 211.97/41.59 $tdef_$_type_470, $tdef_$_type_4850, $tdef_$_type_4913, $tdef_$_type_493, % 211.97/41.59 $tdef_$_type_4976, $tdef_$_type_5030, $tdef_$_type_5093, $tdef_$_type_5300, % 211.97/41.59 $tdef_$_type_5330, $tdef_$_type_5354, $tdef_$_type_5384, $tdef_$_type_5414, % 211.97/41.59 $tdef_$_type_5438, $tdef_$_type_547, $tdef_$_type_5471, $tdef_$_type_5495, % 211.97/41.59 $tdef_$_type_550, $tdef_$_type_5522, $tdef_$_type_5921, $tdef_$_type_594, % 211.97/41.59 $tdef_$_type_6134, $tdef_$_type_6347, $tdef_$_type_640, $tdef_$_type_6542, % 211.97/41.59 $tdef_$_type_6755, $tdef_$_type_6968, $tdef_$_type_7181, $tdef_$_type_7394, % 211.97/41.59 $tdef_$_type_7589, $tdef_$_type_7802, $tdef_$_type_7997, $tdef_$_type_8139, % 211.97/41.59 $tdef_$_type_8158, $tdef_$_type_8172, $tdef_$_type_8327, $tdef_$_type_836, % 211.97/41.59 $tdef_$_type_8377, $tdef_$_type_8427, $tdef_$_type_8469, $tdef_$_type_8519, % 211.97/41.59 $tdef_$_type_8595, $tdef_$_type_8704, $tdef_$_type_8748, $tdef_$_type_8784, % 211.97/41.59 $tdef_$_type_8828, $tdef_$_type_8840, $tdef_$_type_8847, $tdef_$_type_8904, % 211.97/41.59 $tdef_$_type_8909, $tdef_$_type_8915, $tdef_$_type_8935, $tdef_$_type_8976, % 211.97/41.59 $tdef_$_type_9034, $tdef_$_type_9046, $tdef_$_type_9212, $tdef_$_type_9218, % 211.97/41.59 $tdef_$_type_9228, $tdef_$_type_929, $tdef_$_type_99424, $tdef_$_type_99548, % 211.97/41.59 $tdef_Coq.Bool.Bool.reflect, $tdef_Coq.FSets.FSetPositive.PositiveSet.elt, % 211.97/41.59 $tdef_Coq.FSets.FSetPositive.PositiveSet.t, % 211.97/41.59 $tdef_Coq.FSets.FSetPositive.PositiveSet.tree, $tdef_Coq.Init.Byte.byte, % 211.97/41.59 $tdef_Coq.Init.Datatypes.CompareSpecT, $tdef_Coq.Init.Datatypes.bool, % 211.97/41.59 $tdef_Coq.Init.Datatypes.comparison, $tdef_Coq.Init.Datatypes.list, % 211.97/41.59 $tdef_Coq.Init.Datatypes.nat, $tdef_Coq.Init.Datatypes.option, % 211.97/41.59 $tdef_Coq.Init.Datatypes.prod, $tdef_Coq.Init.Datatypes.sum, % 211.97/41.59 $tdef_Coq.Init.Datatypes.unit, $tdef_Coq.Init.Specif.sig, % 211.97/41.59 $tdef_Coq.Init.Specif.sig2, $tdef_Coq.Init.Specif.sigT, % 211.97/41.59 $tdef_Coq.Init.Specif.sigT2, $tdef_Coq.Init.Specif.sumbool, % 211.97/41.59 $tdef_Coq.Init.Specif.sumor, $tdef_Coq.Numbers.BinNums.N, % 211.97/41.59 $tdef_Coq.Numbers.BinNums.Z, $tdef_Coq.Numbers.BinNums.positive, % 211.97/41.59 $tdef_Coq.PArith.BinPosDef.Pos.mask, $tdef_Coq.QArith.QArith_base.Q, % 211.97/41.59 $tdef_Coq.Reals.RIneq.nonzeroreal, $tdef_Coq.Reals.Rdefinitions.R, % 211.97/41.59 $tdef_Coq.Reals.Rfunctions.Z_spec, % 211.97/41.59 $tdef_Coq.Relations.Relation_Definitions.relation, % 211.97/41.59 $tdef_Coq.Strings.Ascii.ascii, $tdef_Coq.Strings.String.string, % 211.97/41.59 $tdef_Coq.Structures.OrderedType.Compare, % 211.97/41.59 $tdef_Coq.Structures.OrderedTypeEx.N_as_OT.t, % 211.97/41.59 $tdef_Coq.Structures.OrderedTypeEx.Nat_as_OT.t, % 211.97/41.59 $tdef_Coq.Structures.OrderedTypeEx.PositiveOrderedTypeBits.t, % 211.97/41.59 $tdef_Coq.Structures.OrderedTypeEx.Positive_as_OT.t, % 211.97/41.59 $tdef_Coq.Structures.OrderedTypeEx.String_as_OT.t, % 211.97/41.59 $tdef_Coq.Structures.OrderedTypeEx.Z_as_OT.t, % 211.97/41.59 $tdef_Coq.Structures.OrdersTac.ord, $tdef_Coq.Vectors.Fin.t, % 211.97/41.59 $tdef_Coq.Vectors.VectorDef.t, $tdef_Coq.ZArith.Znumtheory.Euclid, % 211.97/41.59 $tdef_Coq.ZArith.Zpower.Zdiv_rest_proofs, $tdef_Coq.micromega.Env.Env, % 211.97/41.59 $tdef_Coq.micromega.EnvRing.Mon, $tdef_Coq.micromega.EnvRing.PExpr, % 211.97/41.59 $tdef_Coq.micromega.EnvRing.Pol, $tdef_Coq.micromega.RingMicromega.Formula, % 211.97/41.59 $tdef_Coq.micromega.RingMicromega.Op1, $tdef_Coq.micromega.RingMicromega.Op2, % 211.97/41.59 $tdef_Coq.micromega.Tauto.GFormula, $tdef_Coq.setoid_ring.Field_theory.FExpr, % 211.97/41.59 $tdef_Coq.setoid_ring.Field_theory.linear, % 211.97/41.59 $tdef_Coq.setoid_ring.Field_theory.rsplit, % 211.97/41.59 $tdef_Coq.setoid_ring.Ring_polynom.Mon, % 211.97/41.59 $tdef_Coq.setoid_ring.Ring_polynom.PExpr, % 211.97/41.59 $tdef_Coq.setoid_ring.Ring_polynom.Pol, % 211.97/41.59 $tdef_Coq.setoid_ring.Ring_theory.ring_kind, $tdef_Prop, $tdef_Type, % 211.97/41.59 Coq.Arith.Between.bet_emp, Coq.Arith.Between.bet_eq, % 211.97/41.59 Coq.Arith.Compare_dec.not_eq, Coq.Arith.EqNat.eq_eq_nat, % 211.97/41.59 Coq.Arith.EqNat.eq_nat_eq, Coq.Arith.EqNat.eq_nat_refl, Coq.Arith.Gt.gt_le_S, % 211.97/41.59 Coq.Arith.Le.le_S_n, Coq.Arith.Lt.le_lt_or_eq, Coq.Arith.Lt.lt_n_S, % 211.97/41.59 Coq.Arith.Lt.nat_total_order, Coq.Arith.Lt.neq_0_lt, % 211.97/41.59 Coq.Arith.PeanoNat.Nat.Private_OrderTac.IsTotal.lt_total, % 211.97/41.59 Coq.Arith.PeanoNat.Nat.Private_OrderTac.Tac.eq_lt, % 211.97/41.59 Coq.Arith.PeanoNat.Nat.Private_OrderTac.Tac.eq_neq, % 211.97/41.59 Coq.Arith.PeanoNat.Nat.Private_OrderTac.Tac.eq_refl, % 211.97/41.59 Coq.Arith.PeanoNat.Nat.Private_OrderTac.Tac.eq_sym, % 211.97/41.59 Coq.Arith.PeanoNat.Nat.Private_OrderTac.Tac.eq_trans, % 211.97/41.59 Coq.Arith.PeanoNat.Nat.Private_OrderTac.Tac.le_antisym, % 211.97/41.59 Coq.Arith.PeanoNat.Nat.Private_OrderTac.Tac.le_lt_trans, % 211.97/41.59 Coq.Arith.PeanoNat.Nat.Private_OrderTac.Tac.le_neq_lt, % 211.97/41.59 Coq.Arith.PeanoNat.Nat.Private_OrderTac.Tac.le_refl, % 211.97/41.59 Coq.Arith.PeanoNat.Nat.Private_OrderTac.Tac.lt_eq, % 211.97/41.59 Coq.Arith.PeanoNat.Nat.Private_OrderTac.Tac.lt_irrefl, % 211.97/41.59 Coq.Arith.PeanoNat.Nat.Private_OrderTac.Tac.lt_trans, % 211.97/41.59 Coq.Arith.PeanoNat.Nat.Private_OrderTac.Tac.neq_eq, % 211.97/41.59 Coq.Arith.PeanoNat.Nat.Private_OrderTac.Tac.neq_sym, % 211.97/41.59 Coq.Arith.PeanoNat.Nat.Private_OrderTac.Tac.not_ge_lt, % 211.97/41.59 Coq.Arith.PeanoNat.Nat.Private_OrderTac.Tac.not_gt_le, % 211.97/41.59 Coq.Arith.PeanoNat.Nat.Private_OrderTac.Tac.not_neq_eq, % 211.97/41.59 Coq.Arith.PeanoNat.Nat.Private_Tac.eq_neq, % 211.97/41.59 Coq.Arith.PeanoNat.Nat.Private_Tac.eq_refl, % 211.97/41.59 Coq.Arith.PeanoNat.Nat.Private_Tac.eq_sym, % 211.97/41.59 Coq.Arith.PeanoNat.Nat.Private_Tac.eq_trans, % 211.97/41.59 Coq.Arith.PeanoNat.Nat.Private_Tac.le_antisym, % 211.97/41.59 Coq.Arith.PeanoNat.Nat.Private_Tac.le_neq_lt, % 211.97/41.59 Coq.Arith.PeanoNat.Nat.Private_Tac.lt_irrefl, % 211.97/41.59 Coq.Arith.PeanoNat.Nat.Private_Tac.neq_eq, % 211.97/41.59 Coq.Arith.PeanoNat.Nat.Private_Tac.neq_sym, % 211.97/41.59 Coq.Arith.PeanoNat.Nat.Private_Tac.not_neq_eq, Coq.Arith.PeanoNat.Nat.add_0_l, % 211.97/41.59 Coq.Arith.PeanoNat.Nat.add_0_r, Coq.Arith.PeanoNat.Nat.add_assoc, % 211.97/41.59 Coq.Arith.PeanoNat.Nat.add_comm, Coq.Arith.PeanoNat.Nat.add_le_mono, % 211.97/41.59 Coq.Arith.PeanoNat.Nat.add_le_mono_l, Coq.Arith.PeanoNat.Nat.add_wd, % 211.97/41.59 Coq.Arith.PeanoNat.Nat.eq_equiv, Coq.Arith.PeanoNat.Nat.eq_le_incl, % 211.97/41.59 Coq.Arith.PeanoNat.Nat.eq_stepl, Coq.Arith.PeanoNat.Nat.gcd_comm, % 211.97/41.59 Coq.Arith.PeanoNat.Nat.le_0_l, Coq.Arith.PeanoNat.Nat.le_antisymm, % 211.97/41.59 Coq.Arith.PeanoNat.Nat.le_gt_cases, Coq.Arith.PeanoNat.Nat.le_preorder, % 211.97/41.59 Coq.Arith.PeanoNat.Nat.le_stepl, Coq.Arith.PeanoNat.Nat.le_stepr, % 211.97/41.59 Coq.Arith.PeanoNat.Nat.le_succ_l, Coq.Arith.PeanoNat.Nat.le_trans, % 211.97/41.59 Coq.Arith.PeanoNat.Nat.le_wd, Coq.Arith.PeanoNat.Nat.lt_0_1, % 211.97/41.59 Coq.Arith.PeanoNat.Nat.lt_0_succ, Coq.Arith.PeanoNat.Nat.lt_1_2, % 211.97/41.59 Coq.Arith.PeanoNat.Nat.lt_eq_cases, Coq.Arith.PeanoNat.Nat.lt_le_incl, % 211.97/41.59 Coq.Arith.PeanoNat.Nat.lt_le_trans, Coq.Arith.PeanoNat.Nat.lt_stepl, % 211.97/41.59 Coq.Arith.PeanoNat.Nat.lt_stepr, Coq.Arith.PeanoNat.Nat.lt_succ_diag_r, % 211.97/41.59 Coq.Arith.PeanoNat.Nat.lt_succ_r, Coq.Arith.PeanoNat.Nat.lt_total, % 211.97/41.59 Coq.Arith.PeanoNat.Nat.lt_trichotomy, Coq.Arith.PeanoNat.Nat.lt_wd, % 211.97/41.59 Coq.Arith.PeanoNat.Nat.max_l, Coq.Arith.PeanoNat.Nat.max_r, % 211.97/41.59 Coq.Arith.PeanoNat.Nat.min_l, Coq.Arith.PeanoNat.Nat.mul_0_l, % 211.97/41.59 Coq.Arith.PeanoNat.Nat.mul_0_r, Coq.Arith.PeanoNat.Nat.mul_1_l, % 211.97/41.59 Coq.Arith.PeanoNat.Nat.mul_1_r, Coq.Arith.PeanoNat.Nat.mul_assoc, % 211.97/41.59 Coq.Arith.PeanoNat.Nat.mul_cancel_l, Coq.Arith.PeanoNat.Nat.mul_comm, % 211.97/41.59 Coq.Arith.PeanoNat.Nat.mul_wd, Coq.Arith.PeanoNat.Nat.neq_0_lt_0, % 211.97/41.59 Coq.Arith.PeanoNat.Nat.neq_sym, Coq.Arith.PeanoNat.Nat.one_succ, % 211.97/41.59 Coq.Arith.PeanoNat.Nat.pow_nonzero, Coq.Arith.PeanoNat.Nat.pred_succ, % 211.97/41.59 Coq.Arith.PeanoNat.Nat.succ_wd, Coq.Arith.PeanoNat.Nat.two_succ, % 211.97/41.59 Coq.Bool.Bool.Is_true_eq_left, Coq.Bool.Bool.Is_true_eq_right, % 211.97/41.59 Coq.Bool.Bool.andb_true_r, Coq.Bool.Bool.diff_false_true, % 211.97/41.59 Coq.Bool.Bool.eq_bool_prop_elim, Coq.Bool.Bool.eq_iff_eq_true, % 211.97/41.59 Coq.Bool.Bool.eq_true_false_abs, Coq.Bool.Bool.eq_true_iff_eq, % 211.97/41.59 Coq.Bool.Bool.not_false_is_true, Coq.Bool.Bool.not_true_is_false, % 211.97/41.59 Coq.Bool.Bool.orb_true_intro, Coq.Bool.Bool.trans_eq_bool, % 211.97/41.59 Coq.Init.Datatypes.comparison_eq_stable, Coq.Init.Datatypes.list_ind, % 211.97/41.59 Coq.Init.Datatypes.nat_ind, Coq.Init.Peano.f_equal2_nat, % 211.97/41.59 Coq.Init.Peano.f_equal_nat, Coq.Init.Peano.le_S, Coq.Init.Peano.le_n, % 211.97/41.59 Coq.Init.Peano.not_eq_S, Coq.Init.Specif.proj2_sig, Coq.Init.Wf.Acc_inv, % 211.97/41.59 Coq.Lists.List.map_ext, Coq.Logic.Decidable.dec_not_not, % 211.97/41.59 Coq.Logic.Decidable.not_not_iff, Coq.Logic.EqdepFacts.UIP_shift_on, % 211.97/41.59 Coq.Logic.EqdepFacts.eq_dep1_intro, Coq.Logic.EqdepFacts.eq_dep_intro, % 211.97/41.59 Coq.Logic.EqdepFacts.eq_indd, Coq.Logic.EqdepFacts.internal_eq_sym_internal, % 211.97/41.59 Coq.Logic.Eqdep_dec.K_dec, Coq.Logic.Eqdep_dec.K_dec_on, % 211.97/41.59 Coq.Logic.Eqdep_dec.UIP_dec, Coq.Logic.Eqdep_dec.eq_dep_eq_dec, % 211.97/41.59 Coq.Logic.Eqdep_dec.eq_proofs_unicity, Coq.Logic.Eqdep_dec.eq_proofs_unicity_on, % 211.97/41.59 Coq.NArith.BinNat.N.Private_OrderTac.IsTotal.lt_total, % 211.97/41.59 Coq.NArith.BinNat.N.Private_OrderTac.Tac.eq_neq, % 211.97/41.59 Coq.NArith.BinNat.N.Private_OrderTac.Tac.eq_refl, % 211.97/41.59 Coq.NArith.BinNat.N.Private_OrderTac.Tac.eq_sym, % 211.97/41.59 Coq.NArith.BinNat.N.Private_OrderTac.Tac.eq_trans, % 211.97/41.59 Coq.NArith.BinNat.N.Private_OrderTac.Tac.le_antisym, % 211.97/41.59 Coq.NArith.BinNat.N.Private_OrderTac.Tac.le_lt_trans, % 211.97/41.59 Coq.NArith.BinNat.N.Private_OrderTac.Tac.le_neq_lt, % 211.97/41.59 Coq.NArith.BinNat.N.Private_OrderTac.Tac.le_refl, % 211.97/41.59 Coq.NArith.BinNat.N.Private_OrderTac.Tac.lt_eq, % 211.97/41.59 Coq.NArith.BinNat.N.Private_OrderTac.Tac.lt_irrefl, % 211.97/41.59 Coq.NArith.BinNat.N.Private_OrderTac.Tac.lt_trans, % 211.97/41.59 Coq.NArith.BinNat.N.Private_OrderTac.Tac.neq_eq, % 211.97/41.59 Coq.NArith.BinNat.N.Private_OrderTac.Tac.neq_sym, % 211.97/41.59 Coq.NArith.BinNat.N.Private_OrderTac.Tac.not_ge_lt, % 211.97/41.59 Coq.NArith.BinNat.N.Private_OrderTac.Tac.not_gt_le, % 211.97/41.59 Coq.NArith.BinNat.N.Private_OrderTac.Tac.not_neq_eq, % 211.97/41.59 Coq.NArith.BinNat.N.Private_Tac.eq_neq, Coq.NArith.BinNat.N.Private_Tac.eq_refl, % 211.97/41.59 Coq.NArith.BinNat.N.Private_Tac.eq_sym, % 211.97/41.59 Coq.NArith.BinNat.N.Private_Tac.eq_trans, % 211.97/41.59 Coq.NArith.BinNat.N.Private_Tac.le_antisym, % 211.97/41.59 Coq.NArith.BinNat.N.Private_Tac.le_neq_lt, % 211.97/41.59 Coq.NArith.BinNat.N.Private_Tac.lt_irrefl, % 211.97/41.59 Coq.NArith.BinNat.N.Private_Tac.neq_eq, Coq.NArith.BinNat.N.Private_Tac.neq_sym, % 211.97/41.59 Coq.NArith.BinNat.N.Private_Tac.not_neq_eq, Coq.NArith.BinNat.N.add_0_l, % 211.97/41.59 Coq.NArith.BinNat.N.add_0_r, Coq.NArith.BinNat.N.add_assoc, % 211.97/41.59 Coq.NArith.BinNat.N.add_comm, Coq.NArith.BinNat.N.eq_equiv, % 211.97/41.59 Coq.NArith.BinNat.N.eq_le_incl, Coq.NArith.BinNat.N.eq_stepl, % 211.97/41.59 Coq.NArith.BinNat.N.le_0_l, Coq.NArith.BinNat.N.le_gt_cases, % 211.97/41.59 Coq.NArith.BinNat.N.le_preorder, Coq.NArith.BinNat.N.le_stepl, % 211.97/41.59 Coq.NArith.BinNat.N.le_stepr, Coq.NArith.BinNat.N.le_wd, % 211.97/41.59 Coq.NArith.BinNat.N.lt_0_1, Coq.NArith.BinNat.N.lt_1_2, % 211.97/41.59 Coq.NArith.BinNat.N.lt_eq_cases, Coq.NArith.BinNat.N.lt_le_trans, % 211.97/41.59 Coq.NArith.BinNat.N.lt_stepl, Coq.NArith.BinNat.N.lt_stepr, % 211.97/41.59 Coq.NArith.BinNat.N.lt_succ_diag_r, Coq.NArith.BinNat.N.lt_total, % 211.97/41.59 Coq.NArith.BinNat.N.lt_trichotomy, Coq.NArith.BinNat.N.mul_0_l, % 211.97/41.59 Coq.NArith.BinNat.N.mul_1_l, Coq.NArith.BinNat.N.mul_assoc, % 211.97/41.59 Coq.NArith.BinNat.N.mul_cancel_l, Coq.NArith.BinNat.N.mul_comm, % 211.97/41.59 Coq.NArith.BinNat.N.neq_0_lt_0, Coq.NArith.BinNat.N.neq_sym, % 211.97/41.59 Coq.NArith.BinNat.N.one_succ, Coq.NArith.BinNat.N.pow_nonzero, % 211.97/41.59 Coq.NArith.BinNat.N.pred_succ, Coq.Numbers.BinNums.positive_ind, % 211.97/41.59 Coq.PArith.BinPos.Pos.Private_Tac.eq_neq, % 211.97/41.59 Coq.PArith.BinPos.Pos.Private_Tac.eq_refl, % 211.97/41.59 Coq.PArith.BinPos.Pos.Private_Tac.eq_sym, % 211.97/41.59 Coq.PArith.BinPos.Pos.Private_Tac.eq_trans, % 211.97/41.59 Coq.PArith.BinPos.Pos.Private_Tac.le_antisym, % 211.97/41.59 Coq.PArith.BinPos.Pos.Private_Tac.le_neq_lt, % 211.97/41.59 Coq.PArith.BinPos.Pos.Private_Tac.lt_irrefl, % 211.97/41.59 Coq.PArith.BinPos.Pos.Private_Tac.neq_eq, % 211.97/41.59 Coq.PArith.BinPos.Pos.Private_Tac.neq_sym, % 211.97/41.59 Coq.PArith.BinPos.Pos.Private_Tac.not_neq_eq, Coq.PArith.BinPos.Pos.eq_equiv, % 211.97/41.60 Coq.PArith.BinPos.Pos.iter_swap_gen, Coq.PArith.BinPos.Pos.lt_total, % 211.97/41.60 Coq.PArith.Pnat.Pos2Nat.inj, Coq.QArith.QArith_base.Q_Setoid, % 211.97/41.60 Coq.Reals.DiscrR.IZR_eq, Coq.Reals.RIneq.IZR_neq, Coq.Reals.RIneq.Rdichotomy, % 211.97/41.60 Coq.Reals.RIneq.Req_ge, Coq.Reals.RIneq.Req_ge_sym, Coq.Reals.RIneq.Req_le, % 211.97/41.60 Coq.Reals.RIneq.Req_le_sym, Coq.Reals.RIneq.Rge_le, % 211.97/41.60 Coq.Reals.RIneq.Rgt_eq_compat, Coq.Reals.RIneq.Rlt_eq_compat, % 211.97/41.60 Coq.Reals.RIneq.Rlt_irrefl, Coq.Reals.RIneq.Rlt_le, % 211.97/41.60 Coq.Reals.RIneq.Rmult_eq_compat_l, Coq.Reals.RIneq.Rmult_eq_compat_r, % 211.97/41.60 Coq.Reals.RIneq.Ropp_eq_compat, Coq.Reals.RIneq.Ropp_involutive, % 211.97/41.60 Coq.Reals.RIneq.Rplus_eq_compat_l, Coq.Reals.RIneq.Rplus_eq_compat_r, % 211.97/41.60 Coq.Reals.RIneq.eq_IZR, Coq.Reals.RIneq.f_equal_R, Coq.Reals.Raxioms.Rmult_comm, % 211.97/41.60 Coq.Setoids.Setoid.Seq_refl, % 211.97/41.60 Coq.Structures.OrderedTypeEx.PositiveOrderedTypeBits.eq_sym, % 211.97/41.60 Coq.ZArith.BinInt.Z.Private_OrderTac.IsTotal.lt_total, % 211.97/41.60 Coq.ZArith.BinInt.Z.Private_OrderTac.Tac.eq_le, % 211.97/41.60 Coq.ZArith.BinInt.Z.Private_OrderTac.Tac.eq_lt, % 211.97/41.60 Coq.ZArith.BinInt.Z.Private_OrderTac.Tac.eq_neq, % 211.97/41.60 Coq.ZArith.BinInt.Z.Private_OrderTac.Tac.eq_refl, % 211.97/41.60 Coq.ZArith.BinInt.Z.Private_OrderTac.Tac.eq_sym, % 211.97/41.60 Coq.ZArith.BinInt.Z.Private_OrderTac.Tac.eq_trans, % 211.97/41.60 Coq.ZArith.BinInt.Z.Private_OrderTac.Tac.le_antisym, % 211.97/41.60 Coq.ZArith.BinInt.Z.Private_OrderTac.Tac.le_lt_trans, % 211.97/41.60 Coq.ZArith.BinInt.Z.Private_OrderTac.Tac.le_neq_lt, % 211.97/41.60 Coq.ZArith.BinInt.Z.Private_OrderTac.Tac.le_refl, % 211.97/41.60 Coq.ZArith.BinInt.Z.Private_OrderTac.Tac.lt_eq, % 211.97/41.60 Coq.ZArith.BinInt.Z.Private_OrderTac.Tac.lt_irrefl, % 211.97/41.60 Coq.ZArith.BinInt.Z.Private_OrderTac.Tac.lt_trans, % 211.97/41.60 Coq.ZArith.BinInt.Z.Private_OrderTac.Tac.neq_eq, % 211.97/41.60 Coq.ZArith.BinInt.Z.Private_OrderTac.Tac.neq_sym, % 211.97/41.60 Coq.ZArith.BinInt.Z.Private_OrderTac.Tac.not_ge_lt, % 211.97/41.60 Coq.ZArith.BinInt.Z.Private_OrderTac.Tac.not_gt_le, % 211.97/41.60 Coq.ZArith.BinInt.Z.Private_OrderTac.Tac.not_neq_eq, % 211.97/41.60 Coq.ZArith.BinInt.Z.Private_Tac.eq_neq, Coq.ZArith.BinInt.Z.Private_Tac.eq_refl, % 211.97/41.60 Coq.ZArith.BinInt.Z.Private_Tac.eq_sym, % 211.97/41.60 Coq.ZArith.BinInt.Z.Private_Tac.eq_trans, % 211.97/41.60 Coq.ZArith.BinInt.Z.Private_Tac.le_antisym, % 211.97/41.60 Coq.ZArith.BinInt.Z.Private_Tac.le_neq_lt, % 211.97/41.60 Coq.ZArith.BinInt.Z.Private_Tac.lt_irrefl, % 211.97/41.60 Coq.ZArith.BinInt.Z.Private_Tac.neq_eq, Coq.ZArith.BinInt.Z.Private_Tac.neq_sym, % 211.97/41.60 Coq.ZArith.BinInt.Z.Private_Tac.not_neq_eq, Coq.ZArith.BinInt.Z.abs_eq, % 211.97/41.60 Coq.ZArith.BinInt.Z.add_0_l, Coq.ZArith.BinInt.Z.add_0_r, % 211.97/41.60 Coq.ZArith.BinInt.Z.add_assoc, Coq.ZArith.BinInt.Z.add_cancel_l, % 211.97/41.60 Coq.ZArith.BinInt.Z.add_cancel_r, Coq.ZArith.BinInt.Z.add_comm, % 211.97/41.60 Coq.ZArith.BinInt.Z.add_le_mono, Coq.ZArith.BinInt.Z.add_le_mono_l, % 211.97/41.60 Coq.ZArith.BinInt.Z.add_le_mono_r, Coq.ZArith.BinInt.Z.add_lt_mono_l, % 211.97/41.60 Coq.ZArith.BinInt.Z.add_shuffle0, Coq.ZArith.BinInt.Z.add_shuffle1, % 211.97/41.60 Coq.ZArith.BinInt.Z.eq_decidable, Coq.ZArith.BinInt.Z.eq_equiv, % 211.97/41.60 Coq.ZArith.BinInt.Z.eq_le_incl, Coq.ZArith.BinInt.Z.eq_mul_0, % 211.97/41.60 Coq.ZArith.BinInt.Z.eq_mul_0_l, Coq.ZArith.BinInt.Z.eq_opp_l, % 211.97/41.60 Coq.ZArith.BinInt.Z.eq_opp_r, Coq.ZArith.BinInt.Z.eq_stepl, % 211.97/41.60 Coq.ZArith.BinInt.Z.eq_sym_iff, Coq.ZArith.BinInt.Z.gcd_comm, % 211.97/41.60 Coq.ZArith.BinInt.Z.gt_lt, Coq.ZArith.BinInt.Z.le_antisymm, % 211.97/41.60 Coq.ZArith.BinInt.Z.le_decidable, Coq.ZArith.BinInt.Z.le_ge_cases, % 211.97/41.60 Coq.ZArith.BinInt.Z.le_gt_cases, Coq.ZArith.BinInt.Z.le_lt_trans, % 211.97/41.60 Coq.ZArith.BinInt.Z.le_preorder, Coq.ZArith.BinInt.Z.le_refl, % 211.97/41.60 Coq.ZArith.BinInt.Z.le_stepl, Coq.ZArith.BinInt.Z.le_stepr, % 211.97/41.60 Coq.ZArith.BinInt.Z.le_succ_l, Coq.ZArith.BinInt.Z.le_trans, % 211.97/41.60 Coq.ZArith.BinInt.Z.le_wd, Coq.ZArith.BinInt.Z.lt_0_1, % 211.97/41.60 Coq.ZArith.BinInt.Z.lt_1_2, Coq.ZArith.BinInt.Z.lt_ge_cases, % 211.97/41.60 Coq.ZArith.BinInt.Z.lt_le_incl, Coq.ZArith.BinInt.Z.lt_le_trans, % 211.97/41.60 Coq.ZArith.BinInt.Z.lt_stepl, Coq.ZArith.BinInt.Z.lt_stepr, % 211.97/41.60 Coq.ZArith.BinInt.Z.lt_succ_r, Coq.ZArith.BinInt.Z.lt_total, % 211.97/41.60 Coq.ZArith.BinInt.Z.lt_trichotomy, Coq.ZArith.BinInt.Z.max_l, % 211.97/41.60 Coq.ZArith.BinInt.Z.max_r, Coq.ZArith.BinInt.Z.max_spec, % 211.97/41.60 Coq.ZArith.BinInt.Z.min_l, Coq.ZArith.BinInt.Z.min_r, % 211.97/41.60 Coq.ZArith.BinInt.Z.mul_0_l, Coq.ZArith.BinInt.Z.mul_0_r, % 211.97/41.60 Coq.ZArith.BinInt.Z.mul_1_l, Coq.ZArith.BinInt.Z.mul_1_r, % 211.97/41.60 Coq.ZArith.BinInt.Z.mul_add_distr_l, Coq.ZArith.BinInt.Z.mul_assoc, % 211.97/41.60 Coq.ZArith.BinInt.Z.mul_cancel_l, Coq.ZArith.BinInt.Z.mul_comm, % 211.97/41.60 Coq.ZArith.BinInt.Z.mul_nonneg_nonneg, Coq.ZArith.BinInt.Z.mul_opp_l, % 211.97/41.60 Coq.ZArith.BinInt.Z.mul_reg_l, Coq.ZArith.BinInt.Z.mul_reg_r, % 211.97/41.60 Coq.ZArith.BinInt.Z.mul_shuffle0, Coq.ZArith.BinInt.Z.mul_shuffle3, % 211.97/41.60 Coq.ZArith.BinInt.Z.neq_sym, Coq.ZArith.BinInt.Z.one_succ, % 211.97/41.60 Coq.ZArith.BinInt.Z.opp_0, Coq.ZArith.BinInt.Z.opp_inj, % 211.97/41.60 Coq.ZArith.BinInt.Z.opp_inj_wd, Coq.ZArith.BinInt.Z.opp_involutive, % 211.97/41.60 Coq.ZArith.BinInt.Z.opp_nonneg_nonpos, Coq.ZArith.BinInt.Z.opp_pos_neg, % 211.97/41.60 Coq.ZArith.BinInt.Z.sgn_null, Coq.ZArith.BinInt.Z.sub_0_r, % 211.97/41.60 Coq.ZArith.BinInt.Z.sub_diag, Coq.ZArith.BinInt.Z.succ_pred, % 211.97/41.60 Coq.ZArith.BinInt.Z_eq_mult, Coq.ZArith.BinInt.Zeq_minus, % 211.97/41.60 Coq.ZArith.BinInt.Zplus_eq_compat, Coq.ZArith.BinInt.Zpos_eq, % 211.97/41.60 Coq.ZArith.BinInt.Zsucc_eq_compat, Coq.ZArith.Zcompare.Zcompare_eq_case, % 211.97/41.60 Coq.ZArith.Zorder.Znot_le_gt, Coq.ZArith.Zorder.not_Zeq, % 211.97/41.60 Coq.ZArith.auxiliary.Zegal_left, Coq.ZArith.auxiliary.Zle_left, % 211.97/41.60 Coq.micromega.EnvRing.Mphi_morph, Coq.micromega.EnvRing.env_morph, % 211.97/41.60 Coq.micromega.RingMicromega.cleb_sound, % 211.97/41.60 Coq.micromega.ZMicromega.Vars.Facts.MP.Dec.F.E_ST, % 211.97/41.60 Coq.micromega.ZMicromega.Vars.Facts.MP.Dec.F.Equal_ST, % 211.97/41.60 Coq.micromega.ZMicromega.Vars.Facts.MP.Dec.F.In_eq_iff, % 211.97/41.60 Coq.micromega.ZMicromega.Vars.Facts.MP.Dec.FSetDecideAuxiliary.dec_eq, % 211.97/41.60 Coq.micromega.ZMicromega.Vars.Facts.MP.Dec.FSetDecideAuxiliary.eq_refl_iff, % 211.97/41.60 Coq.omega.OmegaLemmas.OMEGA1, Coq.omega.OmegaLemmas.OMEGA2, % 211.97/41.60 Coq.omega.OmegaLemmas.OMEGA5, Coq.omega.OmegaLemmas.OMEGA6, % 211.97/41.60 Coq.omega.OmegaLemmas.OMEGA8, Coq.omega.OmegaLemmas.new_var, % 211.97/41.60 Coq.omega.PreOmega.Z.div_0_r_ext, Coq.omega.PreOmega.Z.mod_0_r_ext, % 211.97/41.60 Coq.omega.PreOmega.Z.quot_0_r_ext, Coq.omega.PreOmega.Z.rem_0_r_ext, % 211.97/41.60 Coq.setoid_ring.Field_theory.AF_AR, % 211.97/41.60 Coq.setoid_ring.Field_theory.rmul_ext_Proper, % 211.97/41.60 Coq.setoid_ring.InitialRing.gen_phiZ_ext, Coq.setoid_ring.Ring_theory.ARdistr_r, % 211.97/41.60 Coq.setoid_ring.Ring_theory.ARmul_0_l, Coq.setoid_ring.Ring_theory.ARmul_0_r, % 211.97/41.60 Coq.setoid_ring.Ring_theory.ARmul_1_l, Coq.setoid_ring.Ring_theory.ARmul_1_r, % 211.97/41.60 Coq.setoid_ring.Ring_theory.ARmul_assoc, Coq.setoid_ring.Ring_theory.ARmul_comm, % 211.97/41.60 Coq.setoid_ring.Ring_theory.ARopp_mul_l, Coq.setoid_ring.Ring_theory.ARopp_zero, % 211.97/41.60 Coq.setoid_ring.Ring_theory.ARsub_def, Coq.setoid_ring.Ring_theory.Eq_ext, % 211.97/41.60 Coq.setoid_ring.Ring_theory.Eq_s_ext, Coq.setoid_ring.Ring_theory.Eqsth, % 211.97/41.60 Coq.setoid_ring.Ring_theory.Rth_ARth, Coq.setoid_ring.Ring_theory.Smorph0, % 211.97/41.60 Coq.setoid_ring.Ring_theory.Smorph_add, Coq.setoid_ring.Ring_theory.mk_reqe, % 211.97/41.60 Coq.setoid_ring.Ring_theory.morph0, Coq.setoid_ring.Ring_theory.morph1, % 211.97/41.60 Coq.setoid_ring.Ring_theory.morph_add, Coq.setoid_ring.Ring_theory.morph_eq, % 211.97/41.60 Coq.setoid_ring.Ring_theory.morph_mul, Coq.setoid_ring.Ring_theory.morph_opp, % 211.97/41.60 Coq.setoid_ring.Ring_theory.morph_sub, Coq.setoid_ring.Ring_theory.rpow_pow_N, % 211.97/41.60 _HAMMER_COQ_FALSE, _HAMMER_COQ_TRUE, _HAMMER_COQ_TYPE_TYPE % 211.97/41.60 % 211.97/41.60 Those formulas are unsatisfiable: % 211.97/41.60 --------------------------------- % 211.97/41.60 % 211.97/41.60 Begin of proof % 212.20/41.60 | % 212.20/41.60 | CLOSE: (_HAMMER_GOAL) is inconsistent. % 212.20/41.60 | % 212.20/41.60 End of proof % 212.20/41.60 % SZS output end Proof for theBenchmark % 212.20/41.60 % 212.20/41.60 41169ms %------------------------------------------------------------------------------