G4Plus---1.5.2.THM-Prf.s

%------------------------------------------------------------------------------
% File     : G4Plus---1.5.2
% Problem  : SEV672+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : g4plus.sh /export/starexec/sandbox/benchmark/theBenchmark.p 300

% Computer : n007.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 12 07:13:51 PM UTC 2026

% Result   : Theorem 15.80s 15.86s
% Output   : Proof 15.80s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12  % Problem  : SEV672+1 : TPTP v9.3.0. Released v9.3.0.
% 0.12/0.13  % Command  : g4plus.sh /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.16/0.33  % Computer : n007.cluster.edu
% 0.16/0.33  % Model    : x86_64 x86_64
% 0.16/0.33  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.33  % Memory   : 8042.1875MB
% 0.16/0.33  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.16/0.33  % CPULimit : 300
% 0.16/0.33  % WCLimit  : 300
% 0.16/0.33  % DateTime : Mon May 11 14:06:39 EDT 2026
% 0.16/0.33  % CPUTime  : 
% 15.80/15.86  % SZS status Theorem
% 15.80/15.86  % SZS output start Proof
% 15.80/15.86  
% 15.80/15.86  ===============================================================
% 15.80/15.86  TPTP Problem: _HAMMER_GOAL (conjecture with 3118 axiom(s))
% 15.80/15.86    Axioms: [_HAMMER_COQ_TRUE,_HAMMER_COQ_FALSE,_HAMMER_COQ_TYPE_TYPE,$_case_Coq.Init.Datatypes.bool$113326,$_case_Coq.Init.Datatypes.bool$113543,$_case_Coq.Init.Datatypes.bool$166,$_case_Coq.Init.Datatypes.bool$34518,$_case_Coq.Init.Datatypes.bool$34849,$_case_Coq.Init.Datatypes.list$128598,$_case_Coq.Init.Datatypes.list$128685,$_case_Coq.Init.Datatypes.nat$109001,$_case_Coq.Init.Datatypes.nat$109110,$_case_Coq.Init.Datatypes.nat$109204,$_case_Coq.Init.Datatypes.nat$111104,$_case_Coq.Init.Datatypes.nat$113965,$_case_Coq.Init.Datatypes.nat$136884,$_case_Coq.Init.Datatypes.nat$139501,$_case_Coq.Init.Datatypes.nat$139523,$_case_Coq.Init.Datatypes.nat$150278,$_case_Coq.Init.Datatypes.nat$150387,$_case_Coq.Init.Datatypes.nat$150481,$_case_Coq.Init.Datatypes.nat$150586,$_case_Coq.Init.Datatypes.nat$150695,$_case_Coq.Init.Datatypes.nat$150789,$_case_Coq.Init.Datatypes.nat$33979,$_case_Coq.Init.Datatypes.nat$34103,$_case_Coq.Init.Datatypes.nat$34211,$_case_Coq.Init.Datatypes.nat$34601,$_case_Coq.Init.Datatypes.nat$34914,$_case_Coq.Init.Datatypes.nat$35257,$_case_Coq.Init.Datatypes.nat$35379,$_case_Coq.Init.Datatypes.nat$35482,$_case_Coq.Init.Datatypes.prod$134502,$_case_Coq.Numbers.BinNums.Z$139518,$_case_Coq.Numbers.BinNums.positive$141708,$_case_Stlc.STLC.tm$112908,$_def_$_let_var_6_p_139567_139570,$_def_$_let_var_6_p_139569_139571,$_def_Coq.Arith.EqNat.eq_nat,$_def_Coq.Arith.PeanoNat.Nat.add,$_def_Coq.Arith.PeanoNat.Nat.divide,$_def_Coq.Arith.PeanoNat.Nat.eq,$_def_Coq.Arith.PeanoNat.Nat.eqf,$_def_Coq.Arith.PeanoNat.Nat.le,$_def_Coq.Arith.PeanoNat.Nat.log2_iter,$_def_Coq.Arith.PeanoNat.Nat.lt,$_def_Coq.Arith.PeanoNat.Nat.max,$_def_Coq.Arith.PeanoNat.Nat.pred,$_def_Coq.Arith.PeanoNat.Nat.recursion,$_def_Coq.Arith.PeanoNat.Nat.sub,$_def_Coq.Arith.PeanoNat.Nat.succ,$_def_Coq.Arith.PeanoNat.Nat.t,$_def_Coq.Arith.PeanoNat.Nat.tail_add,$_def_Coq.Arith.PeanoNat.Nat.zero,$_def_Coq.Arith.Plus.tail_plus,$_def_Coq.Arith.Wf_nat.ltof,$_def_Coq.Bool.Bool.Is_true,$_def_Coq.Bool.Bool.eqb,$_def_Coq.Bool.Bool.ifb,$_def_Coq.Bool.Bvector.Bvector,$_def_Coq.Bool.Zerob.zerob,$_def_Coq.FSets.FSetPositive.PositiveSet.E.bits_lt,$_def_Coq.FSets.FSetPositive.PositiveSet.E.eq,$_def_Coq.FSets.FSetPositive.PositiveSet.E.lt,$_def_Coq.FSets.FSetPositive.PositiveSet.E.t,$_def_Coq.FSets.FSetPositive.PositiveSet.Equal,$_def_Coq.FSets.FSetPositive.PositiveSet.In,$_def_Coq.FSets.FSetPositive.PositiveSet.Subset,$_def_Coq.FSets.FSetPositive.PositiveSet.elt,$_def_Coq.FSets.FSetPositive.PositiveSet.empty,$_def_Coq.FSets.FSetPositive.PositiveSet.eq,$_def_Coq.FSets.FSetPositive.PositiveSet.mem,$_def_Coq.FSets.FSetPositive.PositiveSet.t,$_def_Coq.Init.Byte.byte_of_byte,$_def_Coq.Init.Datatypes.CompOpp,$_def_Coq.Init.Datatypes.ID,$_def_Coq.Init.Datatypes.IDProp,$_def_Coq.Init.Datatypes.andb,$_def_Coq.Init.Datatypes.app,$_def_Coq.Init.Datatypes.fst,$_def_Coq.Init.Datatypes.id,$_def_Coq.Init.Datatypes.implb,$_def_Coq.Init.Datatypes.nat_rect,$_def_Coq.Init.Datatypes.negb,$_def_Coq.Init.Datatypes.orb,$_def_Coq.Init.Datatypes.snd,$_def_Coq.Init.Datatypes.xorb,$_def_Coq.Init.Decimal.int_of_int,$_def_Coq.Init.Decimal.nzhead,$_def_Coq.Init.Decimal.uint_of_uint,$_def_Coq.Init.Logic_Type.notT,$_def_Coq.Init.Nat.add,$_def_Coq.Init.Nat.compare,$_def_Coq.Init.Nat.div2,$_def_Coq.Init.Nat.double,$_def_Coq.Init.Nat.eqb,$_def_Coq.Init.Nat.even,$_def_Coq.Init.Nat.leb,$_def_Coq.Init.Nat.log2_iter,$_def_Coq.Init.Nat.max,$_def_Coq.Init.Nat.min,$_def_Coq.Init.Nat.mul,$_def_Coq.Init.Nat.pow,$_def_Coq.Init.Nat.pred,$_def_Coq.Init.Nat.sub,$_def_Coq.Init.Nat.succ,$_def_Coq.Init.Nat.t,$_def_Coq.Init.Nat.tail_add,$_def_Coq.Init.Nat.zero,$_def_Coq.Init.Peano.IsSucc,$_def_Coq.Init.Peano.ge,$_def_Coq.Init.Peano.gt,$_def_Coq.Init.Peano.lt,$_def_Coq.Init.Specif.Exc,$_def_Coq.Init.Specif.except,$_def_Coq.Init.Specif.proj1_sig,$_def_Coq.Init.Wf.well_founded,$_def_Coq.Lists.List.In,$_def_Coq.Lists.List.fold_left,$_def_Coq.Lists.List.fold_right,$_def_Coq.Lists.List.hd,$_def_Coq.Lists.List.nth,$_def_Coq.Lists.SetoidList.transpose,$_def_Coq.Lists.SetoidList.transpose2,$_def_Coq.Lists.SetoidList.transpose_restr,$_def_Coq.Lists.SetoidList.transpose_restr2,$_def_Coq.Logic.Decidable.decidable,$_def_Coq.Logic.EqdepFacts.UIP_on_,$_def_Coq.NArith.BinNat.N.eq,$_def_Coq.NArith.BinNat.N.eqf,$_def_Coq.NArith.BinNat.N.le,$_def_Coq.NArith.BinNat.N.lt,$_def_Coq.NArith.BinNat.N.recursion,$_def_Coq.NArith.BinNat.N.t,$_def_Coq.NArith.BinNat.N.zero,$_def_Coq.NArith.BinNatDef.N.add,$_def_Coq.NArith.BinNatDef.N.div2,$_def_Coq.NArith.BinNatDef.N.even,$_def_Coq.NArith.BinNatDef.N.max,$_def_Coq.NArith.BinNatDef.N.min,$_def_Coq.NArith.BinNatDef.N.mul,$_def_Coq.NArith.BinNatDef.N.pred,$_def_Coq.NArith.BinNatDef.N.succ,$_def_Coq.NArith.BinNatDef.N.t,$_def_Coq.NArith.BinNatDef.N.testbit,$_def_Coq.NArith.BinNatDef.N.to_nat,$_def_Coq.NArith.BinNatDef.N.zero,$_def_Coq.NArith.Ndigits.eqf,$_def_Coq.PArith.BinPos.Pos.div2,$_def_Coq.PArith.BinPos.Pos.eq,$_def_Coq.PArith.BinPos.Pos.iter,$_def_Coq.PArith.BinPos.Pos.iter_op,$_def_Coq.PArith.BinPos.Pos.t,$_def_Coq.PArith.BinPosDef.Pos.compare,$_def_Coq.PArith.BinPosDef.Pos.div2,$_def_Coq.PArith.BinPosDef.Pos.eqb,$_def_Coq.PArith.BinPosDef.Pos.iter,$_def_Coq.PArith.BinPosDef.Pos.iter_op,$_def_Coq.PArith.BinPosDef.Pos.max,$_def_Coq.PArith.BinPosDef.Pos.min,$_def_Coq.PArith.BinPosDef.Pos.mul,$_def_Coq.PArith.BinPosDef.Pos.of_succ_nat,$_def_Coq.PArith.BinPosDef.Pos.sub,$_def_Coq.PArith.BinPosDef.Pos.succ,$_def_Coq.PArith.BinPosDef.Pos.t,$_def_Coq.QArith.QArith_base.Qden,$_def_Coq.QArith.QArith_base.Qnum,$_def_Coq.Reals.RIneq.Rsqr,$_def_Coq.Reals.Rdefinitions.Rgt,$_def_Coq.Reals.Rdefinitions.Rle,$_def_Coq.Relations.Relation_Definitions.relation,$_def_Coq.Setoids.Setoid.Setoid_Theory,$_def_Coq.Sets.Relations_1.Relation,$_def_Coq.Structures.DecidableTypeEx.N_as_DT.eq,$_def_Coq.Structures.DecidableTypeEx.N_as_DT.lt,$_def_Coq.Structures.DecidableTypeEx.N_as_DT.t,$_def_Coq.Structures.DecidableTypeEx.Nat_as_DT.eq,$_def_Coq.Structures.DecidableTypeEx.Nat_as_DT.lt,$_def_Coq.Structures.DecidableTypeEx.Nat_as_DT.t,$_def_Coq.Structures.DecidableTypeEx.Positive_as_DT.eq,$_def_Coq.Structures.DecidableTypeEx.Positive_as_DT.lt,$_def_Coq.Structures.DecidableTypeEx.Positive_as_DT.t,$_def_Coq.Structures.DecidableTypeEx.Z_as_DT.eq,$_def_Coq.Structures.DecidableTypeEx.Z_as_DT.lt,$_def_Coq.Structures.DecidableTypeEx.Z_as_DT.t,$_def_Coq.Structures.GenericMinMax.gmax,$_def_Coq.Structures.GenericMinMax.gmin,$_def_Coq.Structures.OrderedTypeEx.N_as_OT.eq,$_def_Coq.Structures.OrderedTypeEx.N_as_OT.lt,$_def_Coq.Structures.OrderedTypeEx.N_as_OT.t,$_def_Coq.Structures.OrderedTypeEx.Nat_as_OT.eq,$_def_Coq.Structures.OrderedTypeEx.Nat_as_OT.lt,$_def_Coq.Structures.OrderedTypeEx.Nat_as_OT.t,$_def_Coq.Structures.OrderedTypeEx.PositiveOrderedTypeBits.bits_lt,$_def_Coq.Structures.OrderedTypeEx.PositiveOrderedTypeBits.eq,$_def_Coq.Structures.OrderedTypeEx.PositiveOrderedTypeBits.lt,$_def_Coq.Structures.OrderedTypeEx.PositiveOrderedTypeBits.t,$_def_Coq.Structures.OrderedTypeEx.Positive_as_OT.eq,$_def_Coq.Structures.OrderedTypeEx.Positive_as_OT.lt,$_def_Coq.Structures.OrderedTypeEx.Positive_as_OT.t,$_def_Coq.Structures.OrderedTypeEx.String_as_OT.lt,$_def_Coq.Structures.OrderedTypeEx.String_as_OT.t,$_def_Coq.Structures.OrderedTypeEx.Z_as_OT.eq,$_def_Coq.Structures.OrderedTypeEx.Z_as_OT.lt,$_def_Coq.Structures.OrderedTypeEx.Z_as_OT.t,$_def_Coq.ZArith.BinInt.Z.Private_Div.Quot2Div.div,$_def_Coq.ZArith.BinInt.Z.Private_Div.Quot2Div.modulo,$_def_Coq.ZArith.BinInt.Z.divide,$_def_Coq.ZArith.BinInt.Z.eq,$_def_Coq.ZArith.BinInt.Z.eqf,$_def_Coq.ZArith.BinInt.Z.le,$_def_Coq.ZArith.BinInt.Z.lt,$_def_Coq.ZArith.BinInt.Z.t,$_def_Coq.ZArith.BinInt.Z.to_pos,$_def_Coq.ZArith.BinInt.Z.zero,$_def_Coq.ZArith.BinInt.Zne,$_def_Coq.ZArith.BinIntDef.Z.abs,$_def_Coq.ZArith.BinIntDef.Z.abs_N,$_def_Coq.ZArith.BinIntDef.Z.add,$_def_Coq.ZArith.BinIntDef.Z.compare,$_def_Coq.ZArith.BinIntDef.Z.div,$_def_Coq.ZArith.BinIntDef.Z.even,$_def_Coq.ZArith.BinIntDef.Z.max,$_def_Coq.ZArith.BinIntDef.Z.min,$_def_Coq.ZArith.BinIntDef.Z.modulo,$_def_Coq.ZArith.BinIntDef.Z.mul,$_def_Coq.ZArith.BinIntDef.Z.odd,$_def_Coq.ZArith.BinIntDef.Z.of_N,$_def_Coq.ZArith.BinIntDef.Z.opp,$_def_Coq.ZArith.BinIntDef.Z.pow,$_def_Coq.ZArith.BinIntDef.Z.sub,$_def_Coq.ZArith.BinIntDef.Z.succ,$_def_Coq.ZArith.BinIntDef.Z.t,$_def_Coq.ZArith.BinIntDef.Z.to_N,$_def_Coq.ZArith.BinIntDef.Z.to_pos,$_def_Coq.ZArith.BinIntDef.Z.zero,$_def_Coq.ZArith.Zbool.Zeq_bool,$_def_Coq.ZArith.Zeven.Zeven,$_def_Coq.ZArith.Zeven.Zodd,$_def_Coq.ZArith.Zlogarithm.Is_power,$_def_Coq.micromega.Env.Env,$_def_Coq.micromega.Refl.make_conj,$_def_Coq.micromega.Refl.make_impl,$_def_Coq.micromega.RingMicromega.PolC,$_def_Coq.micromega.RingMicromega.PolEnv,$_def_Coq.micromega.ZMicromega.Vars.E.bits_lt,$_def_Coq.micromega.ZMicromega.Vars.E.eq,$_def_Coq.micromega.ZMicromega.Vars.E.lt,$_def_Coq.micromega.ZMicromega.Vars.E.t,$_def_Coq.micromega.ZMicromega.Vars.elt,$_def_Coq.micromega.ZMicromega.Vars.eq,$_def_Coq.micromega.ZMicromega.Vars.t,$_def_Coq.micromega.ZMicromega.coneMember,$_def_Coq.omega.PreOmega.Z_of_N',$_def_Coq.omega.PreOmega.Z_of_nat',$_def_Coq.omega.PreOmega.Zneg',$_def_Coq.omega.PreOmega.Zpos',$_def_Coq.setoid_ring.ArithRing.protected_to_nat,$_def_Coq.setoid_ring.InitialRing.NotConstant,$_def_Coq.setoid_ring.InitialRing.Nword,$_def_Coq.setoid_ring.InitialRing.gen_phiPOS,$_def_Coq.setoid_ring.InitialRing.gen_phiPOS1,$_def_Coq.setoid_ring.Ring_polynom.mkmult_pow,$_def_Coq.setoid_ring.Ring_tac.ring_subst_niter,$_def_Coq.setoid_ring.Ring_theory.IDphi,$_def_Coq.setoid_ring.Ring_theory.SRopp,$_def_Coq.setoid_ring.Ring_theory.SRsub,$_def_Coq.setoid_ring.Ring_theory.id_phi_N,$_def_Coq.setoid_ring.Ring_theory.pow_N,$_def_Coq.setoid_ring.Ring_theory.pow_pos,$_def_Hammer.Tactics.Reconstr.rdone,$_def_Hammer.Tactics.Tactics.rdone,$_def_PLF.Imp.X,$_def_PLF.Imp.Y,$_def_PLF.Imp.empty_st,$_def_PLF.Imp.state,$_def_PLF.Maps.eqb_string,$_def_PLF.Maps.t_update,$_def_PLF.Maps.total_map,$_def_PLF.Smallstep.CImp.cmultistep,$_def_PLF.Smallstep.normal_form,$_def_PLF.Smallstep.normal_form_of,$_def_PLF.Smallstep.normalizing,$_def_PLF.Smallstep.prog,$_def_PLF.Smallstep.relation,$_def_PLF.Smallstep.stack,$_def_PLF.Smallstep.stack_multistep,$_def_PLF.Smallstep.step_normal_form,$_def_Stlc.STLC.subst,$_def_Stlc.STLC.substi_rec,$_def_Stlc.STLC.tm_rec,$_def_Stlc.STLC.tm_rect,$_def_Stlc.STLC.ty_rec,$_def_Stlc.STLC.ty_rect,$_def_Stlc.STLC.x,$_discrim_Coq.Bool.Bool.ReflectT$Coq.Bool.Bool.ReflectF,$_discrim_Coq.FSets.FSetPositive.PositiveSet.Leaf$Coq.FSets.FSetPositive.PositiveSet.Node,$_discrim_Coq.Init.Byte.x00$Coq.Init.Byte.x01,$_discrim_Coq.Init.Datatypes.CompEqT$Coq.Init.Datatypes.CompLtT,$_discrim_Coq.Init.Datatypes.Eq$Coq.Init.Datatypes.Lt,$_discrim_Coq.Init.Datatypes.O$Coq.Init.Datatypes.S,$_discrim_Coq.Init.Datatypes.Some$Coq.Init.Datatypes.None,$_discrim_Coq.Init.Datatypes.inl$Coq.Init.Datatypes.inr,$_discrim_Coq.Init.Datatypes.nil$Coq.Init.Datatypes.cons,$_discrim_Coq.Init.Datatypes.true$Coq.Init.Datatypes.false,$_discrim_Coq.Init.Decimal.Decimal$Coq.Init.Decimal.DecimalExp,$_discrim_Coq.Init.Decimal.Nil$Coq.Init.Decimal.D0,$_discrim_Coq.Init.Decimal.Pos$Coq.Init.Decimal.Neg,$_discrim_Coq.Init.Specif.inleft$Coq.Init.Specif.inright,$_discrim_Coq.Init.Specif.left$Coq.Init.Specif.right,$_discrim_Coq.Numbers.BinNums.N0$Coq.Numbers.BinNums.Npos,$_discrim_Coq.Numbers.BinNums.Z0$Coq.Numbers.BinNums.Zpos,$_discrim_Coq.Numbers.BinNums.xI$Coq.Numbers.BinNums.xO,$_discrim_Coq.PArith.BinPos.Pos.IsNul$Coq.PArith.BinPos.Pos.IsPos,$_discrim_Coq.PArith.BinPos.Pos.PeanoOne$Coq.PArith.BinPos.Pos.PeanoSucc,$_discrim_Coq.PArith.BinPosDef.Pos.IsNul$Coq.PArith.BinPosDef.Pos.IsPos,$_discrim_Coq.Reals.Rfunctions.ZintNull$Coq.Reals.Rfunctions.ZintPos,$_discrim_Coq.Strings.String.EmptyString$Coq.Strings.String.String,$_discrim_Coq.Structures.OrderedType.LT$Coq.Structures.OrderedType.EQ,$_discrim_Coq.Structures.OrdersTac.OEQ$Coq.Structures.OrdersTac.OLT,$_discrim_Coq.Vectors.Fin.F1$Coq.Vectors.Fin.FS,$_discrim_Coq.Vectors.Vector.nil$Coq.Vectors.Vector.cons,$_discrim_Coq.Vectors.VectorDef.nil$Coq.Vectors.VectorDef.cons,$_discrim_Coq.micromega.EnvRing.PEc$Coq.micromega.EnvRing.PEX,$_discrim_Coq.micromega.EnvRing.Pc$Coq.micromega.EnvRing.Pinj,$_discrim_Coq.micromega.EnvRing.mon0$Coq.micromega.EnvRing.zmon,$_discrim_Coq.micromega.RMicromega.C0$Coq.micromega.RMicromega.C1,$_discrim_Coq.micromega.RingMicromega.Equal$Coq.micromega.RingMicromega.NonEqual,$_discrim_Coq.micromega.RingMicromega.OpEq$Coq.micromega.RingMicromega.OpNEq,$_discrim_Coq.micromega.RingMicromega.PsatzIn$Coq.micromega.RingMicromega.PsatzSquare,$_discrim_Coq.micromega.Tauto.TT$Coq.micromega.Tauto.FF,$_discrim_Coq.micromega.VarMap.Empty$Coq.micromega.VarMap.Elt,$_discrim_Coq.micromega.ZMicromega.DoneProof$Coq.micromega.ZMicromega.RatProof,$_discrim_Coq.micromega.ZMicromega.Vars.Leaf$Coq.micromega.ZMicromega.Vars.Node,$_discrim_Coq.setoid_ring.Field_theory.FEO$Coq.setoid_ring.Field_theory.FEI,$_discrim_Coq.setoid_ring.Ring_polynom.PEO$Coq.setoid_ring.Ring_polynom.PEI,$_discrim_Coq.setoid_ring.Ring_polynom.Pc$Coq.setoid_ring.Ring_polynom.Pinj,$_discrim_Coq.setoid_ring.Ring_polynom.mon0$Coq.setoid_ring.Ring_polynom.zmon,$_discrim_Coq.setoid_ring.Ring_theory.Abstract$Coq.setoid_ring.Ring_theory.Computational,$_discrim_Hammer.Tactics.Reconstr.Empty$Hammer.Tactics.Reconstr.AllHyps,$_discrim_PLF.Imp.AExp.ANum$PLF.Imp.AExp.APlus,$_discrim_PLF.Imp.AExp.BTrue$PLF.Imp.AExp.BFalse,$_discrim_PLF.Imp.ANum$PLF.Imp.AId,$_discrim_PLF.Imp.BTrue$PLF.Imp.BFalse,$_discrim_PLF.Imp.BreakImp.CSkip$PLF.Imp.BreakImp.CBreak,$_discrim_PLF.Imp.BreakImp.SContinue$PLF.Imp.BreakImp.SBreak,$_discrim_PLF.Imp.CSkip$PLF.Imp.CAss,$_discrim_PLF.Imp.SPush$PLF.Imp.SLoad,$_discrim_PLF.Imp.aevalR_division.ANum$PLF.Imp.aevalR_division.APlus,$_discrim_PLF.Imp.aevalR_extended.AAny$PLF.Imp.aevalR_extended.ANum,$_discrim_PLF.Smallstep.C$PLF.Smallstep.P,$_discrim_PLF.Smallstep.CImp.CSkip$PLF.Smallstep.CImp.CAss,$_discrim_PLF.Smallstep.Combined.C$PLF.Smallstep.Combined.P,$_discrim_PLF.Smallstep.Temp4.tru$PLF.Smallstep.Temp4.fls,$_discrim_Stlc.STLC.Bool$Stlc.STLC.Arrow,$_discrim_Stlc.STLC.var$Stlc.STLC.app,$_fix_113301_v_CANONICAL_0,$_fix_128730_v_CANONICAL_1,$_fix_141724_v_CANONICAL_0,$_fix_33998_v_CANONICAL_0,$_fix_34144_v_CANONICAL_0,$_fix_34230_v_CANONICAL_0,$_fix_34653_v_CANONICAL_0,$_fix_34955_v_CANONICAL_0,$_inj_Coq.Bool.Bool.ReflectF,$_inj_Coq.Bool.Bool.ReflectT,$_inj_Coq.FSets.FSetPositive.PositiveSet.Node,$_inj_Coq.Init.Datatypes.CompEqT,$_inj_Coq.Init.Datatypes.CompGtT,$_inj_Coq.Init.Datatypes.CompLtT,$_inj_Coq.Init.Datatypes.None,$_inj_Coq.Init.Datatypes.S,$_inj_Coq.Init.Datatypes.Some,$_inj_Coq.Init.Datatypes.cons,$_inj_Coq.Init.Datatypes.inl,$_inj_Coq.Init.Datatypes.inr,$_inj_Coq.Init.Datatypes.nil,$_inj_Coq.Init.Datatypes.pair,$_inj_Coq.Init.Decimal.D0,$_inj_Coq.Init.Decimal.D1,$_inj_Coq.Init.Decimal.D2,$_inj_Coq.Init.Decimal.D3,$_inj_Coq.Init.Decimal.D4,$_inj_Coq.Init.Decimal.D5,$_inj_Coq.Init.Decimal.D6,$_inj_Coq.Init.Decimal.D7,$_inj_Coq.Init.Decimal.D8,$_inj_Coq.Init.Decimal.D9,$_inj_Coq.Init.Decimal.Decimal,$_inj_Coq.Init.Decimal.DecimalExp,$_inj_Coq.Init.Decimal.Neg,$_inj_Coq.Init.Decimal.Pos,$_inj_Coq.Init.Specif.exist,$_inj_Coq.Init.Specif.exist2,$_inj_Coq.Init.Specif.existT,$_inj_Coq.Init.Specif.existT2,$_inj_Coq.Init.Specif.inleft,$_inj_Coq.Init.Specif.inright,$_inj_Coq.Init.Specif.left,$_inj_Coq.Init.Specif.right,$_inj_Coq.Numbers.BinNums.Npos,$_inj_Coq.Numbers.BinNums.Zneg,$_inj_Coq.Numbers.BinNums.Zpos,$_inj_Coq.Numbers.BinNums.xI,$_inj_Coq.Numbers.BinNums.xO,$_inj_Coq.PArith.BinPos.Pos.IsPos,$_inj_Coq.PArith.BinPos.Pos.PeanoSucc,$_inj_Coq.PArith.BinPosDef.Pos.IsPos,$_inj_Coq.QArith.QArith_base.Qmake,$_inj_Coq.Reals.RIneq.mknegreal,$_inj_Coq.Reals.RIneq.mknonnegreal,$_inj_Coq.Reals.RIneq.mknonposreal,$_inj_Coq.Reals.RIneq.mknonzeroreal,$_inj_Coq.Reals.RIneq.mkposreal,$_inj_Coq.Reals.Rfunctions.ZintNeg,$_inj_Coq.Reals.Rfunctions.ZintNull,$_inj_Coq.Reals.Rfunctions.ZintPos,$_inj_Coq.Strings.Ascii.Ascii,$_inj_Coq.Strings.String.String,$_inj_Coq.Structures.OrderedType.EQ,$_inj_Coq.Structures.OrderedType.GT,$_inj_Coq.Structures.OrderedType.LT,$_inj_Coq.Vectors.Fin.F1,$_inj_Coq.Vectors.Fin.FS,$_inj_Coq.Vectors.Vector.cons,$_inj_Coq.Vectors.Vector.nil,$_inj_Coq.Vectors.VectorDef.cons,$_inj_Coq.Vectors.VectorDef.nil,$_inj_Coq.ZArith.Znumtheory.Euclid_intro,$_inj_Coq.ZArith.Zpower.Zdiv_rest_proof,$_inj_Coq.micromega.EnvRing.PEX,$_inj_Coq.micromega.EnvRing.PEadd,$_inj_Coq.micromega.EnvRing.PEc,$_inj_Coq.micromega.EnvRing.PEmul,$_inj_Coq.micromega.EnvRing.PEopp,$_inj_Coq.micromega.EnvRing.PEpow,$_inj_Coq.micromega.EnvRing.PEsub,$_inj_Coq.micromega.EnvRing.PX,$_inj_Coq.micromega.EnvRing.Pc,$_inj_Coq.micromega.EnvRing.Pinj,$_inj_Coq.micromega.EnvRing.vmon,$_inj_Coq.micromega.EnvRing.zmon,$_inj_Coq.micromega.RMicromega.CInv,$_inj_Coq.micromega.RMicromega.CMinus,$_inj_Coq.micromega.RMicromega.CMult,$_inj_Coq.micromega.RMicromega.COpp,$_inj_Coq.micromega.RMicromega.CPlus,$_inj_Coq.micromega.RMicromega.CPow,$_inj_Coq.micromega.RMicromega.CQ,$_inj_Coq.micromega.RMicromega.CZ,$_inj_Coq.micromega.RingMicromega.Build_Formula,$_inj_Coq.micromega.RingMicromega.PsatzAdd,$_inj_Coq.micromega.RingMicromega.PsatzC,$_inj_Coq.micromega.RingMicromega.PsatzIn,$_inj_Coq.micromega.RingMicromega.PsatzMulC,$_inj_Coq.micromega.RingMicromega.PsatzMulE,$_inj_Coq.micromega.RingMicromega.PsatzSquare,$_inj_Coq.micromega.RingMicromega.PsatzZ,$_inj_Coq.micromega.Tauto.A,$_inj_Coq.micromega.Tauto.Cj,$_inj_Coq.micromega.Tauto.D,$_inj_Coq.micromega.Tauto.FF,$_inj_Coq.micromega.Tauto.I,$_inj_Coq.micromega.Tauto.N,$_inj_Coq.micromega.Tauto.TT,$_inj_Coq.micromega.Tauto.X,$_inj_Coq.micromega.VarMap.Branch,$_inj_Coq.micromega.VarMap.Elt,$_inj_Coq.micromega.VarMap.Empty,$_inj_Coq.micromega.ZMicromega.CutProof,$_inj_Coq.micromega.ZMicromega.EnumProof,$_inj_Coq.micromega.ZMicromega.RatProof,$_inj_Coq.micromega.ZMicromega.Vars.Node,$_inj_Coq.setoid_ring.Field_theory.FEI,$_inj_Coq.setoid_ring.Field_theory.FEO,$_inj_Coq.setoid_ring.Field_theory.FEX,$_inj_Coq.setoid_ring.Field_theory.FEadd,$_inj_Coq.setoid_ring.Field_theory.FEc,$_inj_Coq.setoid_ring.Field_theory.FEdiv,$_inj_Coq.setoid_ring.Field_theory.FEinv,$_inj_Coq.setoid_ring.Field_theory.FEmul,$_inj_Coq.setoid_ring.Field_theory.FEopp,$_inj_Coq.setoid_ring.Field_theory.FEpow,$_inj_Coq.setoid_ring.Field_theory.FEsub,$_inj_Coq.setoid_ring.Field_theory.mk_linear,$_inj_Coq.setoid_ring.Field_theory.mk_rsplit,$_inj_Coq.setoid_ring.InitialRing.mkhypo,$_inj_Coq.setoid_ring.Ring_polynom.PEI,$_inj_Coq.setoid_ring.Ring_polynom.PEO,$_inj_Coq.setoid_ring.Ring_polynom.PEX,$_inj_Coq.setoid_ring.Ring_polynom.PEadd,$_inj_Coq.setoid_ring.Ring_polynom.PEc,$_inj_Coq.setoid_ring.Ring_polynom.PEmul,$_inj_Coq.setoid_ring.Ring_polynom.PEopp,$_inj_Coq.setoid_ring.Ring_polynom.PEpow,$_inj_Coq.setoid_ring.Ring_polynom.PEsub,$_inj_Coq.setoid_ring.Ring_polynom.PX,$_inj_Coq.setoid_ring.Ring_polynom.Pc,$_inj_Coq.setoid_ring.Ring_polynom.Pinj,$_inj_Coq.setoid_ring.Ring_polynom.vmon,$_inj_Coq.setoid_ring.Ring_polynom.zmon,$_inj_Coq.setoid_ring.Ring_theory.Computational,$_inj_Coq.setoid_ring.Ring_theory.Morphism,$_inj_PLF.Imp.AExp.AMinus,$_inj_PLF.Imp.AExp.AMult,$_inj_PLF.Imp.AExp.ANum,$_inj_PLF.Imp.AExp.APlus,$_inj_PLF.Imp.AExp.BAnd,$_inj_PLF.Imp.AExp.BEq,$_inj_PLF.Imp.AExp.BLe,$_inj_PLF.Imp.AExp.BNot,$_inj_PLF.Imp.AId,$_inj_PLF.Imp.AMinus,$_inj_PLF.Imp.AMult,$_inj_PLF.Imp.ANum,$_inj_PLF.Imp.APlus,$_inj_PLF.Imp.BAnd,$_inj_PLF.Imp.BEq,$_inj_PLF.Imp.BLe,$_inj_PLF.Imp.BNot,$_inj_PLF.Imp.BreakImp.CAss,$_inj_PLF.Imp.BreakImp.CIf,$_inj_PLF.Imp.BreakImp.CSeq,$_inj_PLF.Imp.BreakImp.CWhile,$_inj_PLF.Imp.CAss,$_inj_PLF.Imp.CIf,$_inj_PLF.Imp.CSeq,$_inj_PLF.Imp.CWhile,$_inj_PLF.Imp.SLoad,$_inj_PLF.Imp.SPush,$_inj_PLF.Imp.aevalR_division.ADiv,$_inj_PLF.Imp.aevalR_division.AMinus,$_inj_PLF.Imp.aevalR_division.AMult,$_inj_PLF.Imp.aevalR_division.ANum,$_inj_PLF.Imp.aevalR_division.APlus,$_inj_PLF.Imp.aevalR_extended.AMinus,$_inj_PLF.Imp.aevalR_extended.AMult,$_inj_PLF.Imp.aevalR_extended.ANum,$_inj_PLF.Imp.aevalR_extended.APlus,$_inj_PLF.Smallstep.C,$_inj_PLF.Smallstep.CImp.CAss,$_inj_PLF.Smallstep.CImp.CIf,$_inj_PLF.Smallstep.CImp.CPar,$_inj_PLF.Smallstep.CImp.CSeq,$_inj_PLF.Smallstep.CImp.CWhile,$_inj_PLF.Smallstep.Combined.C,$_inj_PLF.Smallstep.Combined.P,$_inj_PLF.Smallstep.Combined.test,$_inj_PLF.Smallstep.P,$_inj_PLF.Smallstep.Temp4.test,$_inj_Stlc.STLC.Arrow,$_inj_Stlc.STLC.abs,$_inj_Stlc.STLC.app,$_inj_Stlc.STLC.test,$_inj_Stlc.STLC.var,$_inversion_Coq.Arith.Between.P_nth,$_inversion_Coq.Arith.Between.between,$_inversion_Coq.Arith.Between.exists_between,$_inversion_Coq.Arith.Even.even,$_inversion_Coq.Arith.Even.odd,$_inversion_Coq.Bool.Bool.reflect,$_inversion_Coq.FSets.FSetPositive.PositiveSet.ct,$_inversion_Coq.FSets.FSetPositive.PositiveSet.tree,$_inversion_Coq.Init.Byte.byte,$_inversion_Coq.Init.Datatypes.BoolSpec,$_inversion_Coq.Init.Datatypes.CompareSpec,$_inversion_Coq.Init.Datatypes.CompareSpecT,$_inversion_Coq.Init.Datatypes.bool,$_inversion_Coq.Init.Datatypes.comparison,$_inversion_Coq.Init.Datatypes.eq_true,$_inversion_Coq.Init.Datatypes.identity,$_inversion_Coq.Init.Datatypes.list,$_inversion_Coq.Init.Datatypes.nat,$_inversion_Coq.Init.Datatypes.option,$_inversion_Coq.Init.Datatypes.prod,$_inversion_Coq.Init.Datatypes.sum,$_inversion_Coq.Init.Datatypes.unit,$_inversion_Coq.Init.Decimal.decimal,$_inversion_Coq.Init.Decimal.int,$_inversion_Coq.Init.Decimal.uint,$_inversion_Coq.Init.Peano.le,$_inversion_Coq.Init.Specif.sig,$_inversion_Coq.Init.Specif.sig2,$_inversion_Coq.Init.Specif.sigT,$_inversion_Coq.Init.Specif.sigT2,$_inversion_Coq.Init.Specif.sumbool,$_inversion_Coq.Init.Specif.sumor,$_inversion_Coq.Init.Wf.Acc,$_inversion_Coq.Lists.List.Add,$_inversion_Coq.Lists.List.Exists,$_inversion_Coq.Lists.List.Forall,$_inversion_Coq.Lists.List.Forall2,$_inversion_Coq.Lists.List.ForallOrdPairs,$_inversion_Coq.Lists.List.NoDup,$_inversion_Coq.Lists.SetoidList.InA,$_inversion_Coq.Lists.SetoidList.NoDupA,$_inversion_Coq.Lists.SetoidList.eqlistA,$_inversion_Coq.Logic.EqdepFacts.eq_dep,$_inversion_Coq.Logic.EqdepFacts.eq_dep1,$_inversion_Coq.Numbers.BinNums.N,$_inversion_Coq.Numbers.BinNums.Z,$_inversion_Coq.Numbers.BinNums.positive,$_inversion_Coq.PArith.BinPos.Pos.PeanoView,$_inversion_Coq.PArith.BinPos.Pos.SubMaskSpec,$_inversion_Coq.PArith.BinPos.Pos.mask,$_inversion_Coq.PArith.BinPosDef.Pos.mask,$_inversion_Coq.QArith.QArith_base.Q,$_inversion_Coq.Reals.RIneq.negreal,$_inversion_Coq.Reals.RIneq.nonnegreal,$_inversion_Coq.Reals.RIneq.nonposreal,$_inversion_Coq.Reals.RIneq.nonzeroreal,$_inversion_Coq.Reals.RIneq.posreal,$_inversion_Coq.Reals.Rfunctions.Z_spec,$_inversion_Coq.Relations.Relation_Definitions.PER,$_inversion_Coq.Relations.Relation_Definitions.equivalence,$_inversion_Coq.Relations.Relation_Definitions.order,$_inversion_Coq.Relations.Relation_Definitions.preorder,$_inversion_Coq.Relations.Relation_Operators.Desc,$_inversion_Coq.Relations.Relation_Operators.Ltl,$_inversion_Coq.Relations.Relation_Operators.clos_refl,$_inversion_Coq.Relations.Relation_Operators.clos_refl_sym_trans_1n,$_inversion_Coq.Relations.Relation_Operators.clos_refl_sym_trans_n1,$_inversion_Coq.Relations.Relation_Operators.clos_refl_trans,$_inversion_Coq.Relations.Relation_Operators.clos_refl_trans_1n,$_inversion_Coq.Relations.Relation_Operators.clos_refl_trans_n1,$_inversion_Coq.Relations.Relation_Operators.clos_trans,$_inversion_Coq.Relations.Relation_Operators.clos_trans_1n,$_inversion_Coq.Relations.Relation_Operators.clos_trans_n1,$_inversion_Coq.Relations.Relation_Operators.lexprod,$_inversion_Coq.Relations.Relation_Operators.swapprod,$_inversion_Coq.Relations.Relation_Operators.symprod,$_inversion_Coq.Sorting.Sorted.HdRel,$_inversion_Coq.Sorting.Sorted.LocallySorted,$_inversion_Coq.Sorting.Sorted.Sorted,$_inversion_Coq.Sorting.Sorted.StronglySorted,$_inversion_Coq.Strings.Ascii.ascii,$_inversion_Coq.Strings.String.string,$_inversion_Coq.Structures.OrderedType.Compare,$_inversion_Coq.Structures.OrderedTypeEx.String_as_OT.lts,$_inversion_Coq.Structures.OrdersTac.ord,$_inversion_Coq.Vectors.Fin.t,$_inversion_Coq.Vectors.Vector.Forall,$_inversion_Coq.Vectors.Vector.Forall2,$_inversion_Coq.Vectors.Vector.t,$_inversion_Coq.Vectors.VectorDef.Forall,$_inversion_Coq.Vectors.VectorDef.Forall2,$_inversion_Coq.Vectors.VectorDef.t,$_inversion_Coq.ZArith.Znumtheory.Bezout,$_inversion_Coq.ZArith.Znumtheory.Euclid,$_inversion_Coq.ZArith.Znumtheory.Zis_gcd,$_inversion_Coq.ZArith.Znumtheory.prime,$_inversion_Coq.ZArith.Zpower.Zdiv_rest_proofs,$_inversion_Coq.micromega.DeclConstant.DeclaredConstant,$_inversion_Coq.micromega.DeclConstant.GT,$_inversion_Coq.micromega.EnvRing.Mon,$_inversion_Coq.micromega.EnvRing.PExpr,$_inversion_Coq.micromega.EnvRing.Pol,$_inversion_Coq.micromega.OrderedRing.SOR,$_inversion_Coq.micromega.RMicromega.Rcst,$_inversion_Coq.micromega.RingMicromega.Formula,$_inversion_Coq.micromega.RingMicromega.Op1,$_inversion_Coq.micromega.RingMicromega.Op2,$_inversion_Coq.micromega.RingMicromega.Psatz,$_inversion_Coq.micromega.RingMicromega.SORaddon,$_inversion_Coq.micromega.Tauto.GFormula,$_inversion_Coq.micromega.VarMap.t,$_inversion_Coq.micromega.ZMicromega.Vars.Facts.MP.Dec.FSetDecideAuxiliary.FSet_Prop,$_inversion_Coq.micromega.ZMicromega.Vars.Facts.MP.Dec.FSetDecideAuxiliary.FSet_elt_Prop,$_inversion_Coq.micromega.ZMicromega.Vars.ct,$_inversion_Coq.micromega.ZMicromega.Vars.tree,$_inversion_Coq.micromega.ZMicromega.ZArithProof,$_inversion_Coq.micromega.ZMicromega.is_diff_env_elt,$_inversion_Coq.setoid_ring.Field_theory.FExpr,$_inversion_Coq.setoid_ring.Field_theory.almost_field_theory,$_inversion_Coq.setoid_ring.Field_theory.field_theory,$_inversion_Coq.setoid_ring.Field_theory.linear,$_inversion_Coq.setoid_ring.Field_theory.rsplit,$_inversion_Coq.setoid_ring.Field_theory.semi_field_theory,$_inversion_Coq.setoid_ring.InitialRing.hypo,$_inversion_Coq.setoid_ring.Ring_polynom.Mon,$_inversion_Coq.setoid_ring.Ring_polynom.PExpr,$_inversion_Coq.setoid_ring.Ring_polynom.Pol,$_inversion_Coq.setoid_ring.Ring_theory.almost_ring_theory,$_inversion_Coq.setoid_ring.Ring_theory.div_theory,$_inversion_Coq.setoid_ring.Ring_theory.power_theory,$_inversion_Coq.setoid_ring.Ring_theory.ring_eq_ext,$_inversion_Coq.setoid_ring.Ring_theory.ring_kind,$_inversion_Coq.setoid_ring.Ring_theory.ring_morph,$_inversion_Coq.setoid_ring.Ring_theory.ring_theory,$_inversion_Coq.setoid_ring.Ring_theory.semi_morph,$_inversion_Coq.setoid_ring.Ring_theory.semi_ring_theory,$_inversion_Coq.setoid_ring.Ring_theory.sring_eq_ext,$_inversion_Hammer.Tactics.Reconstr.ReconstrT,$_inversion_PLF.Imp.AExp.aevalR,$_inversion_PLF.Imp.AExp.aevalR_first_try.TooHardToRead.aevalR,$_inversion_PLF.Imp.AExp.aevalR_first_try.aevalR,$_inversion_PLF.Imp.AExp.aexp,$_inversion_PLF.Imp.AExp.bexp,$_inversion_PLF.Imp.BreakImp.com,$_inversion_PLF.Imp.BreakImp.result,$_inversion_PLF.Imp.aevalR_division.aevalR,$_inversion_PLF.Imp.aevalR_division.aexp,$_inversion_PLF.Imp.aevalR_extended.aevalR,$_inversion_PLF.Imp.aevalR_extended.aexp,$_inversion_PLF.Imp.aexp,$_inversion_PLF.Imp.bexp,$_inversion_PLF.Imp.ceval,$_inversion_PLF.Imp.com,$_inversion_PLF.Imp.sinstr,$_inversion_PLF.Smallstep.CImp.com,$_inversion_PLF.Smallstep.CImp.cstep,$_inversion_PLF.Smallstep.Combined.step,$_inversion_PLF.Smallstep.Combined.tm,$_inversion_PLF.Smallstep.Combined.value,$_inversion_PLF.Smallstep.SimpleArith1.step,$_inversion_PLF.Smallstep.Temp1.step,$_inversion_PLF.Smallstep.Temp1.value,$_inversion_PLF.Smallstep.Temp2.step,$_inversion_PLF.Smallstep.Temp2.value,$_inversion_PLF.Smallstep.Temp3.step,$_inversion_PLF.Smallstep.Temp3.value,$_inversion_PLF.Smallstep.Temp4.Temp5.step,$_inversion_PLF.Smallstep.Temp4.step,$_inversion_PLF.Smallstep.Temp4.tm,$_inversion_PLF.Smallstep.Temp4.value,$_inversion_PLF.Smallstep.astep,$_inversion_PLF.Smallstep.aval,$_inversion_PLF.Smallstep.bstep,$_inversion_PLF.Smallstep.eval,$_inversion_PLF.Smallstep.multi,$_inversion_PLF.Smallstep.stack_step,$_inversion_PLF.Smallstep.step,$_inversion_PLF.Smallstep.tm,$_inversion_PLF.Smallstep.value,$_inversion_Stlc.STLC.step,$_inversion_Stlc.STLC.substi,$_inversion_Stlc.STLC.tm,$_inversion_Stlc.STLC.ty,$_inversion_Stlc.STLC.value,$_lam_142139,$_lam_142147,$_lam_149467,$_lam_149529,$_lam_31563,$_lam_32206,$_prop_141636,$_prop_141637,$_prop_141638,$_prop_141639,$_prop_141640,$_prop_141641,$_prop_141642,$_prop_141656,$_prop_141657,$_prop_141658,$_prop_32,$_prop_33,$_prop_34,$_prop_35,$_type_101871,$_type_101874,$_type_101888,$_type_101890,$_type_101934,$_type_102,$_type_102761,$_type_102795,$_type_102797,$_type_102799,$_type_102804,$_type_102809,$_type_102817,$_type_102854,$_type_102858,$_type_102861,$_type_102878,$_type_102905,$_type_102913,$_type_102921,$_type_102973,$_type_102977,$_type_102995,$_type_103022,$_type_103030,$_type_103038,$_type_103090,$_type_103096,$_type_105,$_type_107468,$_type_107907,$_type_108568,$_type_108646,$_type_108649,$_type_108883,$_type_108886,$_type_109499,$_type_109503,$_type_109506,$_type_109522,$_type_109524,$_type_109527,$_type_109612,$_type_109663,$_type_109671,$_type_109711,$_type_109731,$_type_109738,$_type_109844,$_type_109864,$_type_109866,$_type_110315,$_type_110366,$_type_110395,$_type_110399,$_type_110466,$_type_110478,$_type_110521,$_type_110533,$_type_110563,$_type_110635,$_type_110639,$_type_110976,$_type_111017,$_type_111282,$_type_111344,$_type_111392,$_type_111446,$_type_111461,$_type_111464,$_type_113836,$_type_113838,$_type_113850,$_type_113852,$_type_113863,$_type_113886,$_type_113888,$_type_113891,$_type_113984,$_type_113987,$_type_113995,$_type_114007,$_type_114010,$_type_114013,$_type_121245,$_type_121700,$_type_121801,$_type_121902,$_type_121992,$_type_122093,$_type_122194,$_type_122295,$_type_122349,$_type_122843,$_type_122906,$_type_122969,$_type_123023,$_type_123086,$_type_123107,$_type_124138,$_type_124202,$_type_124353,$_type_124387,$_type_124559,$_type_124770,$_type_124863,$_type_124956,$_type_125038,$_type_125131,$_type_125213,$_type_125306,$_type_126700,$_type_127115,$_type_127129,$_type_127136,$_type_127754,$_type_127761,$_type_127906,$_type_128081,$_type_128104,$_type_128400,$_type_129008,$_type_129011,$_type_129016,$_type_129019,$_type_130388,$_type_130642,$_type_130705,$_type_130768,$_type_130822,$_type_130885,$_type_131105,$_type_131135,$_type_131159,$_type_131189,$_type_131219,$_type_131243,$_type_131276,$_type_131300,$_type_131327,$_type_131740,$_type_131953,$_type_132166,$_type_132361,$_type_132574,$_type_132787,$_type_133000,$_type_133213,$_type_133408,$_type_133621,$_type_133816,$_type_134247,$_type_134297,$_type_134347,$_type_134389,$_type_134439,$_type_134515,$_type_134723,$_type_134767,$_type_134803,$_type_134847,$_type_134866,$_type_134982,$_type_135084,$_type_136804,$_type_137546,$_type_137644,$_type_138174,$_type_138270,$_type_138466,$_type_138559,$_type_138652,$_type_138734,$_type_138827,$_type_138909,$_type_139002,$_type_139156,$_type_139219,$_type_139282,$_type_139336,$_type_139399,$_type_139430,$_type_139530,$_type_139581,$_type_139754,$_type_139793,$_type_139832,$_type_139936,$_type_139959,$_type_139982,$_type_140005,$_type_140023,$_type_140049,$_type_140067,$_type_140325,$_type_140450,$_type_140575,$_type_140700,$_type_140825,$_type_140950,$_type_141061,$_type_141071,$_type_141300,$_type_141341,$_type_141351,$_type_141399,$_type_141515,$_type_141744,$_type_141886,$_type_141907,$_type_141942,$_type_141950,$_type_141952,$_type_141957,$_type_141959,$_type_141966,$_type_141979,$_type_141984,$_type_141989,$_type_142014,$_type_142079,$_type_142087,$_type_142090,$_type_142093,$_type_142103,$_type_142108,$_type_142114,$_type_142119,$_type_142131,$_type_142151,$_type_142162,$_type_142180,$_type_142183,$_type_142222,$_type_142233,$_type_142258,$_type_142306,$_type_142360,$_type_142384,$_type_142431,$_type_142466,$_type_142468,$_type_142484,$_type_143023,$_type_143026,$_type_143030,$_type_143033,$_type_143051,$_type_143077,$_type_143306,$_type_143335,$_type_143372,$_type_143444,$_type_143469,$_type_143511,$_type_143562,$_type_144097,$_type_144443,$_type_144789,$_type_145112,$_type_145458,$_type_145804,$_type_146150,$_type_146496,$_type_146842,$_type_147165,$_type_147511,$_type_147857,$_type_148180,$_type_148503,$_type_148849,$_type_148858,$_type_148861,$_type_148864,$_type_148888,$_type_148903,$_type_148946,$_type_149007,$_type_149042,$_type_149077,$_type_149080,$_type_149108,$_type_149159,$_type_149186,$_type_149237,$_type_149243,$_type_149255,$_type_149258,$_type_149366,$_type_149375,$_type_149404,$_type_149420,$_type_149423,$_type_149479,$_type_149484,$_type_149541,$_type_149546,$_type_149579,$_type_150184,$_type_150500,$_type_170,$_type_172,$_type_294,$_type_296,$_type_299,$_type_30176,$_type_30183,$_type_30195,$_type_30197,$_type_30200,$_type_30212,$_type_30231,$_type_30252,$_type_311,$_type_31247,$_type_31263,$_type_31495,$_type_31633,$_type_31685,$_type_31760,$_type_31779,$_type_31799,$_type_31804,$_type_31978,$_type_32189,$_type_32246,$_type_323,$_type_32678,$_type_33403,$_type_33416,$_type_33421,$_type_33424,$_type_33426,$_type_33429,$_type_33788,$_type_33790,$_type_33847,$_type_346,$_type_35532,$_type_35537,$_type_35656,$_type_35968,$_type_35971,$_type_35976,$_type_35979,$_type_36289,$_type_36302,$_type_36304,$_type_36315,$_type_36328,$_type_37,$_type_381,$_type_568,$_type_571,$_type_576,$_type_581,$_type_9,$_type_99,$_typeof_Coq.Arith.EqNat.eq_nat,$_typeof_Coq.Arith.PeanoNat.Nat.add,$_typeof_Coq.Arith.PeanoNat.Nat.divide,$_typeof_Coq.Arith.PeanoNat.Nat.eq,$_typeof_Coq.Arith.PeanoNat.Nat.eqf,$_typeof_Coq.Arith.PeanoNat.Nat.le,$_typeof_Coq.Arith.PeanoNat.Nat.log2_iter,$_typeof_Coq.Arith.PeanoNat.Nat.lt,$_typeof_Coq.Arith.PeanoNat.Nat.max,$_typeof_Coq.Arith.PeanoNat.Nat.pred,$_typeof_Coq.Arith.PeanoNat.Nat.recursion,$_typeof_Coq.Arith.PeanoNat.Nat.sub,$_typeof_Coq.Arith.PeanoNat.Nat.succ,$_typeof_Coq.Arith.PeanoNat.Nat.t,$_typeof_Coq.Arith.PeanoNat.Nat.tail_add,$_typeof_Coq.Arith.PeanoNat.Nat.zero,$_typeof_Coq.Arith.Plus.tail_plus,$_typeof_Coq.Arith.Wf_nat.ltof,$_typeof_Coq.Bool.Bool.Is_true,$_typeof_Coq.Bool.Bool.eqb,$_typeof_Coq.Bool.Bool.ifb,$_typeof_Coq.Bool.Bool.reflect,$_typeof_Coq.Bool.Bvector.Bvector,$_typeof_Coq.Bool.Zerob.zerob,$_typeof_Coq.FSets.FSetPositive.PositiveSet.E.bits_lt,$_typeof_Coq.FSets.FSetPositive.PositiveSet.E.eq,$_typeof_Coq.FSets.FSetPositive.PositiveSet.E.lt,$_typeof_Coq.FSets.FSetPositive.PositiveSet.E.t,$_typeof_Coq.FSets.FSetPositive.PositiveSet.Equal,$_typeof_Coq.FSets.FSetPositive.PositiveSet.In,$_typeof_Coq.FSets.FSetPositive.PositiveSet.Leaf,$_typeof_Coq.FSets.FSetPositive.PositiveSet.Node,$_typeof_Coq.FSets.FSetPositive.PositiveSet.Subset,$_typeof_Coq.FSets.FSetPositive.PositiveSet.elt,$_typeof_Coq.FSets.FSetPositive.PositiveSet.empty,$_typeof_Coq.FSets.FSetPositive.PositiveSet.eq,$_typeof_Coq.FSets.FSetPositive.PositiveSet.mem,$_typeof_Coq.FSets.FSetPositive.PositiveSet.t,$_typeof_Coq.FSets.FSetPositive.PositiveSet.tree,$_typeof_Coq.Init.Byte.byte,$_typeof_Coq.Init.Byte.byte_of_byte,$_typeof_Coq.Init.Byte.x00,$_typeof_Coq.Init.Byte.x01,$_typeof_Coq.Init.Byte.x02,$_typeof_Coq.Init.Byte.x03,$_typeof_Coq.Init.Byte.x04,$_typeof_Coq.Init.Byte.x05,$_typeof_Coq.Init.Byte.x06,$_typeof_Coq.Init.Byte.x07,$_typeof_Coq.Init.Byte.x08,$_typeof_Coq.Init.Byte.x09,$_typeof_Coq.Init.Byte.x0a,$_typeof_Coq.Init.Byte.x0b,$_typeof_Coq.Init.Byte.x0c,$_typeof_Coq.Init.Byte.x0d,$_typeof_Coq.Init.Byte.x0e,$_typeof_Coq.Init.Byte.x0f,$_typeof_Coq.Init.Byte.x10,$_typeof_Coq.Init.Byte.x11,$_typeof_Coq.Init.Byte.x12,$_typeof_Coq.Init.Byte.x13,$_typeof_Coq.Init.Byte.x14,$_typeof_Coq.Init.Byte.x15,$_typeof_Coq.Init.Byte.x16,$_typeof_Coq.Init.Byte.x17,$_typeof_Coq.Init.Byte.x18,$_typeof_Coq.Init.Byte.x19,$_typeof_Coq.Init.Byte.x1a,$_typeof_Coq.Init.Byte.x1b,$_typeof_Coq.Init.Byte.x1c,$_typeof_Coq.Init.Byte.x1d,$_typeof_Coq.Init.Byte.x1e,$_typeof_Coq.Init.Byte.x1f,$_typeof_Coq.Init.Byte.x20,$_typeof_Coq.Init.Byte.x21,$_typeof_Coq.Init.Byte.x22,$_typeof_Coq.Init.Byte.x23,$_typeof_Coq.Init.Byte.x24,$_typeof_Coq.Init.Byte.x25,$_typeof_Coq.Init.Byte.x26,$_typeof_Coq.Init.Byte.x27,$_typeof_Coq.Init.Byte.x28,$_typeof_Coq.Init.Byte.x29,$_typeof_Coq.Init.Byte.x2a,$_typeof_Coq.Init.Byte.x2b,$_typeof_Coq.Init.Byte.x2c,$_typeof_Coq.Init.Byte.x2d,$_typeof_Coq.Init.Byte.x2e,$_typeof_Coq.Init.Byte.x2f,$_typeof_Coq.Init.Byte.x30,$_typeof_Coq.Init.Byte.x31,$_typeof_Coq.Init.Byte.x32,$_typeof_Coq.Init.Byte.x33,$_typeof_Coq.Init.Byte.x34,$_typeof_Coq.Init.Byte.x35,$_typeof_Coq.Init.Byte.x36,$_typeof_Coq.Init.Byte.x37,$_typeof_Coq.Init.Byte.x38,$_typeof_Coq.Init.Byte.x39,$_typeof_Coq.Init.Byte.x3a,$_typeof_Coq.Init.Byte.x3b,$_typeof_Coq.Init.Byte.x3c,$_typeof_Coq.Init.Byte.x3d,$_typeof_Coq.Init.Byte.x3e,$_typeof_Coq.Init.Byte.x3f,$_typeof_Coq.Init.Byte.x40,$_typeof_Coq.Init.Byte.x41,$_typeof_Coq.Init.Byte.x42,$_typeof_Coq.Init.Byte.x43,$_typeof_Coq.Init.Byte.x44,$_typeof_Coq.Init.Byte.x45,$_typeof_Coq.Init.Byte.x46,$_typeof_Coq.Init.Byte.x47,$_typeof_Coq.Init.Byte.x48,$_typeof_Coq.Init.Byte.x49,$_typeof_Coq.Init.Byte.x4a,$_typeof_Coq.Init.Byte.x4b,$_typeof_Coq.Init.Byte.x4c,$_typeof_Coq.Init.Byte.x4d,$_typeof_Coq.Init.Byte.x4e,$_typeof_Coq.Init.Byte.x4f,$_typeof_Coq.Init.Byte.x50,$_typeof_Coq.Init.Byte.x51,$_typeof_Coq.Init.Byte.x52,$_typeof_Coq.Init.Byte.x53,$_typeof_Coq.Init.Byte.x54,$_typeof_Coq.Init.Byte.x55,$_typeof_Coq.Init.Byte.x56,$_typeof_Coq.Init.Byte.x57,$_typeof_Coq.Init.Byte.x58,$_typeof_Coq.Init.Byte.x59,$_typeof_Coq.Init.Byte.x5a,$_typeof_Coq.Init.Byte.x5b,$_typeof_Coq.Init.Byte.x5c,$_typeof_Coq.Init.Byte.x5d,$_typeof_Coq.Init.Byte.x5e,$_typeof_Coq.Init.Byte.x5f,$_typeof_Coq.Init.Byte.x60,$_typeof_Coq.Init.Byte.x61,$_typeof_Coq.Init.Byte.x62,$_typeof_Coq.Init.Byte.x63,$_typeof_Coq.Init.Byte.x64,$_typeof_Coq.Init.Byte.x65,$_typeof_Coq.Init.Byte.x66,$_typeof_Coq.Init.Byte.x67,$_typeof_Coq.Init.Byte.x68,$_typeof_Coq.Init.Byte.x69,$_typeof_Coq.Init.Byte.x6a,$_typeof_Coq.Init.Byte.x6b,$_typeof_Coq.Init.Byte.x6c,$_typeof_Coq.Init.Byte.x6d,$_typeof_Coq.Init.Byte.x6e,$_typeof_Coq.Init.Byte.x6f,$_typeof_Coq.Init.Byte.x70,$_typeof_Coq.Init.Byte.x71,$_typeof_Coq.Init.Byte.x72,$_typeof_Coq.Init.Byte.x73,$_typeof_Coq.Init.Byte.x74,$_typeof_Coq.Init.Byte.x75,$_typeof_Coq.Init.Byte.x76,$_typeof_Coq.Init.Byte.x77,$_typeof_Coq.Init.Byte.x78,$_typeof_Coq.Init.Byte.x79,$_typeof_Coq.Init.Byte.x7a,$_typeof_Coq.Init.Byte.x7b,$_typeof_Coq.Init.Byte.x7c,$_typeof_Coq.Init.Byte.x7d,$_typeof_Coq.Init.Byte.x7e,$_typeof_Coq.Init.Byte.x7f,$_typeof_Coq.Init.Byte.x80,$_typeof_Coq.Init.Byte.x81,$_typeof_Coq.Init.Byte.x82,$_typeof_Coq.Init.Byte.x83,$_typeof_Coq.Init.Byte.x84,$_typeof_Coq.Init.Byte.x85,$_typeof_Coq.Init.Byte.x86,$_typeof_Coq.Init.Byte.x87,$_typeof_Coq.Init.Byte.x88,$_typeof_Coq.Init.Byte.x89,$_typeof_Coq.Init.Byte.x8a,$_typeof_Coq.Init.Byte.x8b,$_typeof_Coq.Init.Byte.x8c,$_typeof_Coq.Init.Byte.x8d,$_typeof_Coq.Init.Byte.x8e,$_typeof_Coq.Init.Byte.x8f,$_typeof_Coq.Init.Byte.x90,$_typeof_Coq.Init.Byte.x91,$_typeof_Coq.Init.Byte.x92,$_typeof_Coq.Init.Byte.x93,$_typeof_Coq.Init.Byte.x94,$_typeof_Coq.Init.Byte.x95,$_typeof_Coq.Init.Byte.x96,$_typeof_Coq.Init.Byte.x97,$_typeof_Coq.Init.Byte.x98,$_typeof_Coq.Init.Byte.x99,$_typeof_Coq.Init.Byte.x9a,$_typeof_Coq.Init.Byte.x9b,$_typeof_Coq.Init.Byte.x9c,$_typeof_Coq.Init.Byte.x9d,$_typeof_Coq.Init.Byte.x9e,$_typeof_Coq.Init.Byte.x9f,$_typeof_Coq.Init.Byte.xa0,$_typeof_Coq.Init.Byte.xa1,$_typeof_Coq.Init.Byte.xa2,$_typeof_Coq.Init.Byte.xa3,$_typeof_Coq.Init.Byte.xa4,$_typeof_Coq.Init.Byte.xa5,$_typeof_Coq.Init.Byte.xa6,$_typeof_Coq.Init.Byte.xa7,$_typeof_Coq.Init.Byte.xa8,$_typeof_Coq.Init.Byte.xa9,$_typeof_Coq.Init.Byte.xaa,$_typeof_Coq.Init.Byte.xab,$_typeof_Coq.Init.Byte.xac,$_typeof_Coq.Init.Byte.xad,$_typeof_Coq.Init.Byte.xae,$_typeof_Coq.Init.Byte.xaf,$_typeof_Coq.Init.Byte.xb0,$_typeof_Coq.Init.Byte.xb1,$_typeof_Coq.Init.Byte.xb2,$_typeof_Coq.Init.Byte.xb3,$_typeof_Coq.Init.Byte.xb4,$_typeof_Coq.Init.Byte.xb5,$_typeof_Coq.Init.Byte.xb6,$_typeof_Coq.Init.Byte.xb7,$_typeof_Coq.Init.Byte.xb8,$_typeof_Coq.Init.Byte.xb9,$_typeof_Coq.Init.Byte.xba,$_typeof_Coq.Init.Byte.xbb,$_typeof_Coq.Init.Byte.xbc,$_typeof_Coq.Init.Byte.xbd,$_typeof_Coq.Init.Byte.xbe,$_typeof_Coq.Init.Byte.xbf,$_typeof_Coq.Init.Byte.xc0,$_typeof_Coq.Init.Byte.xc1,$_typeof_Coq.Init.Byte.xc2,$_typeof_Coq.Init.Byte.xc3,$_typeof_Coq.Init.Byte.xc4,$_typeof_Coq.Init.Byte.xc5,$_typeof_Coq.Init.Byte.xc6,$_typeof_Coq.Init.Byte.xc7,$_typeof_Coq.Init.Byte.xc8,$_typeof_Coq.Init.Byte.xc9,$_typeof_Coq.Init.Byte.xca,$_typeof_Coq.Init.Byte.xcb,$_typeof_Coq.Init.Byte.xcc,$_typeof_Coq.Init.Byte.xcd,$_typeof_Coq.Init.Byte.xce,$_typeof_Coq.Init.Byte.xcf,$_typeof_Coq.Init.Byte.xd0,$_typeof_Coq.Init.Byte.xd1,$_typeof_Coq.Init.Byte.xd2,$_typeof_Coq.Init.Byte.xd3,$_typeof_Coq.Init.Byte.xd4,$_typeof_Coq.Init.Byte.xd5,$_typeof_Coq.Init.Byte.xd6,$_typeof_Coq.Init.Byte.xd7,$_typeof_Coq.Init.Byte.xd8,$_typeof_Coq.Init.Byte.xd9,$_typeof_Coq.Init.Byte.xda,$_typeof_Coq.Init.Byte.xdb,$_typeof_Coq.Init.Byte.xdc,$_typeof_Coq.Init.Byte.xdd,$_typeof_Coq.Init.Byte.xde,$_typeof_Coq.Init.Byte.xdf,$_typeof_Coq.Init.Byte.xe0,$_typeof_Coq.Init.Byte.xe1,$_typeof_Coq.Init.Byte.xe2,$_typeof_Coq.Init.Byte.xe3,$_typeof_Coq.Init.Byte.xe4,$_typeof_Coq.Init.Byte.xe5,$_typeof_Coq.Init.Byte.xe6,$_typeof_Coq.Init.Byte.xe7,$_typeof_Coq.Init.Byte.xe8,$_typeof_Coq.Init.Byte.xe9,$_typeof_Coq.Init.Byte.xea,$_typeof_Coq.Init.Byte.xeb,$_typeof_Coq.Init.Byte.xec,$_typeof_Coq.Init.Byte.xed,$_typeof_Coq.Init.Byte.xee,$_typeof_Coq.Init.Byte.xef,$_typeof_Coq.Init.Byte.xf0,$_typeof_Coq.Init.Byte.xf1,$_typeof_Coq.Init.Byte.xf2,$_typeof_Coq.Init.Byte.xf3,$_typeof_Coq.Init.Byte.xf4,$_typeof_Coq.Init.Byte.xf5,$_typeof_Coq.Init.Byte.xf6,$_typeof_Coq.Init.Byte.xf7,$_typeof_Coq.Init.Byte.xf8,$_typeof_Coq.Init.Byte.xf9,$_typeof_Coq.Init.Byte.xfa,$_typeof_Coq.Init.Byte.xfb,$_typeof_Coq.Init.Byte.xfc,$_typeof_Coq.Init.Byte.xfd,$_typeof_Coq.Init.Byte.xfe,$_typeof_Coq.Init.Byte.xff,$_typeof_Coq.Init.Datatypes.CompOpp,$_typeof_Coq.Init.Datatypes.CompareSpecT,$_typeof_Coq.Init.Datatypes.Empty_set,$_typeof_Coq.Init.Datatypes.Eq,$_typeof_Coq.Init.Datatypes.Gt,$_typeof_Coq.Init.Datatypes.ID,$_typeof_Coq.Init.Datatypes.IDProp,$_typeof_Coq.Init.Datatypes.Lt,$_typeof_Coq.Init.Datatypes.None,$_typeof_Coq.Init.Datatypes.O,$_typeof_Coq.Init.Datatypes.S,$_typeof_Coq.Init.Datatypes.Some,$_typeof_Coq.Init.Datatypes.andb,$_typeof_Coq.Init.Datatypes.app,$_typeof_Coq.Init.Datatypes.bool,$_typeof_Coq.Init.Datatypes.comparison,$_typeof_Coq.Init.Datatypes.cons,$_typeof_Coq.Init.Datatypes.false,$_typeof_Coq.Init.Datatypes.fst,$_typeof_Coq.Init.Datatypes.id,$_typeof_Coq.Init.Datatypes.implb,$_typeof_Coq.Init.Datatypes.inl,$_typeof_Coq.Init.Datatypes.inr,$_typeof_Coq.Init.Datatypes.list,$_typeof_Coq.Init.Datatypes.nat,$_typeof_Coq.Init.Datatypes.nat_rect,$_typeof_Coq.Init.Datatypes.negb,$_typeof_Coq.Init.Datatypes.nil,$_typeof_Coq.Init.Datatypes.option,$_typeof_Coq.Init.Datatypes.orb,$_typeof_Coq.Init.Datatypes.pair,$_typeof_Coq.Init.Datatypes.prod,$_typeof_Coq.Init.Datatypes.snd,$_typeof_Coq.Init.Datatypes.sum,$_typeof_Coq.Init.Datatypes.true,$_typeof_Coq.Init.Datatypes.tt,$_typeof_Coq.Init.Datatypes.unit,$_typeof_Coq.Init.Datatypes.xorb,$_typeof_Coq.Init.Decimal.D0,$_typeof_Coq.Init.Decimal.D1,$_typeof_Coq.Init.Decimal.D2,$_typeof_Coq.Init.Decimal.D3,$_typeof_Coq.Init.Decimal.D4,$_typeof_Coq.Init.Decimal.D5,$_typeof_Coq.Init.Decimal.D6,$_typeof_Coq.Init.Decimal.D7,$_typeof_Coq.Init.Decimal.D8,$_typeof_Coq.Init.Decimal.D9,$_typeof_Coq.Init.Decimal.Nil,$_typeof_Coq.Init.Decimal.decimal,$_typeof_Coq.Init.Decimal.int,$_typeof_Coq.Init.Decimal.int_of_int,$_typeof_Coq.Init.Decimal.nzhead,$_typeof_Coq.Init.Decimal.uint,$_typeof_Coq.Init.Decimal.uint_of_uint,$_typeof_Coq.Init.Logic_Type.notT,$_typeof_Coq.Init.Nat.add,$_typeof_Coq.Init.Nat.compare,$_typeof_Coq.Init.Nat.div2,$_typeof_Coq.Init.Nat.double,$_typeof_Coq.Init.Nat.eqb,$_typeof_Coq.Init.Nat.even,$_typeof_Coq.Init.Nat.leb,$_typeof_Coq.Init.Nat.log2_iter,$_typeof_Coq.Init.Nat.max,$_typeof_Coq.Init.Nat.min,$_typeof_Coq.Init.Nat.mul,$_typeof_Coq.Init.Nat.pow,$_typeof_Coq.Init.Nat.pred,$_typeof_Coq.Init.Nat.sub,$_typeof_Coq.Init.Nat.succ,$_typeof_Coq.Init.Nat.t,$_typeof_Coq.Init.Nat.tail_add,$_typeof_Coq.Init.Nat.zero,$_typeof_Coq.Init.Peano.IsSucc,$_typeof_Coq.Init.Peano.ge,$_typeof_Coq.Init.Peano.gt,$_typeof_Coq.Init.Peano.lt,$_typeof_Coq.Init.Specif.Exc,$_typeof_Coq.Init.Specif.except,$_typeof_Coq.Init.Specif.exist,$_typeof_Coq.Init.Specif.existT,$_typeof_Coq.Init.Specif.left,$_typeof_Coq.Init.Specif.proj1_sig,$_typeof_Coq.Init.Specif.right,$_typeof_Coq.Init.Specif.sig,$_typeof_Coq.Init.Specif.sig2,$_typeof_Coq.Init.Specif.sigT,$_typeof_Coq.Init.Specif.sigT2,$_typeof_Coq.Init.Specif.sumbool,$_typeof_Coq.Init.Specif.sumor,$_typeof_Coq.Init.Wf.well_founded,$_typeof_Coq.Lists.List.In,$_typeof_Coq.Lists.List.fold_left,$_typeof_Coq.Lists.List.fold_right,$_typeof_Coq.Lists.List.hd,$_typeof_Coq.Lists.List.nth,$_typeof_Coq.Lists.SetoidList.transpose,$_typeof_Coq.Lists.SetoidList.transpose2,$_typeof_Coq.Lists.SetoidList.transpose_restr,$_typeof_Coq.Lists.SetoidList.transpose_restr2,$_typeof_Coq.Logic.Decidable.decidable,$_typeof_Coq.Logic.EqdepFacts.UIP_on_,$_typeof_Coq.NArith.BinNat.N.eq,$_typeof_Coq.NArith.BinNat.N.eqf,$_typeof_Coq.NArith.BinNat.N.le,$_typeof_Coq.NArith.BinNat.N.lt,$_typeof_Coq.NArith.BinNat.N.recursion,$_typeof_Coq.NArith.BinNat.N.t,$_typeof_Coq.NArith.BinNat.N.zero,$_typeof_Coq.NArith.BinNatDef.N.add,$_typeof_Coq.NArith.BinNatDef.N.div2,$_typeof_Coq.NArith.BinNatDef.N.even,$_typeof_Coq.NArith.BinNatDef.N.max,$_typeof_Coq.NArith.BinNatDef.N.min,$_typeof_Coq.NArith.BinNatDef.N.mul,$_typeof_Coq.NArith.BinNatDef.N.pred,$_typeof_Coq.NArith.BinNatDef.N.succ,$_typeof_Coq.NArith.BinNatDef.N.t,$_typeof_Coq.NArith.BinNatDef.N.testbit,$_typeof_Coq.NArith.BinNatDef.N.to_nat,$_typeof_Coq.NArith.BinNatDef.N.zero,$_typeof_Coq.NArith.Ndigits.eqf,$_typeof_Coq.Numbers.BinNums.N,$_typeof_Coq.Numbers.BinNums.N0,$_typeof_Coq.Numbers.BinNums.Npos,$_typeof_Coq.Numbers.BinNums.Z,$_typeof_Coq.Numbers.BinNums.Z0,$_typeof_Coq.Numbers.BinNums.Zneg,$_typeof_Coq.Numbers.BinNums.Zpos,$_typeof_Coq.Numbers.BinNums.positive,$_typeof_Coq.Numbers.BinNums.xH,$_typeof_Coq.Numbers.BinNums.xI,$_typeof_Coq.Numbers.BinNums.xO,$_typeof_Coq.PArith.BinPos.Pos.IsNeg,$_typeof_Coq.PArith.BinPos.Pos.IsNul,$_typeof_Coq.PArith.BinPos.Pos.PeanoView,$_typeof_Coq.PArith.BinPos.Pos.div2,$_typeof_Coq.PArith.BinPos.Pos.eq,$_typeof_Coq.PArith.BinPos.Pos.iter,$_typeof_Coq.PArith.BinPos.Pos.iter_op,$_typeof_Coq.PArith.BinPos.Pos.mask,$_typeof_Coq.PArith.BinPos.Pos.t,$_typeof_Coq.PArith.BinPosDef.Pos.IsNeg,$_typeof_Coq.PArith.BinPosDef.Pos.IsNul,$_typeof_Coq.PArith.BinPosDef.Pos.IsPos,$_typeof_Coq.PArith.BinPosDef.Pos.compare,$_typeof_Coq.PArith.BinPosDef.Pos.div2,$_typeof_Coq.PArith.BinPosDef.Pos.eqb,$_typeof_Coq.PArith.BinPosDef.Pos.iter,$_typeof_Coq.PArith.BinPosDef.Pos.iter_op,$_typeof_Coq.PArith.BinPosDef.Pos.mask,$_typeof_Coq.PArith.BinPosDef.Pos.max,$_typeof_Coq.PArith.BinPosDef.Pos.min,$_typeof_Coq.PArith.BinPosDef.Pos.mul,$_typeof_Coq.PArith.BinPosDef.Pos.of_succ_nat,$_typeof_Coq.PArith.BinPosDef.Pos.sub,$_typeof_Coq.PArith.BinPosDef.Pos.succ,$_typeof_Coq.PArith.BinPosDef.Pos.t,$_typeof_Coq.QArith.QArith_base.Q,$_typeof_Coq.QArith.QArith_base.Qden,$_typeof_Coq.QArith.QArith_base.Qmake,$_typeof_Coq.QArith.QArith_base.Qnum,$_typeof_Coq.Reals.RIneq.Rsqr,$_typeof_Coq.Reals.RIneq.negreal,$_typeof_Coq.Reals.RIneq.nonnegreal,$_typeof_Coq.Reals.RIneq.nonposreal,$_typeof_Coq.Reals.RIneq.nonzeroreal,$_typeof_Coq.Reals.RIneq.posreal,$_typeof_Coq.Reals.Rdefinitions.R,$_typeof_Coq.Reals.Rdefinitions.R0,$_typeof_Coq.Reals.Rdefinitions.R1,$_typeof_Coq.Reals.Rdefinitions.Rgt,$_typeof_Coq.Reals.Rdefinitions.Rinv,$_typeof_Coq.Reals.Rdefinitions.Rle,$_typeof_Coq.Reals.Rdefinitions.Rlt,$_typeof_Coq.Reals.Rdefinitions.Rmult,$_typeof_Coq.Reals.Rdefinitions.Ropp,$_typeof_Coq.Reals.Rdefinitions.Rplus,$_typeof_Coq.Reals.Rdefinitions.up,$_typeof_Coq.Reals.Rfunctions.Z_spec,$_typeof_Coq.Relations.Relation_Definitions.relation,$_typeof_Coq.Setoids.Setoid.Setoid_Theory,$_typeof_Coq.Sets.Relations_1.Relation,$_typeof_Coq.Strings.Ascii.Ascii,$_typeof_Coq.Strings.Ascii.ascii,$_typeof_Coq.Strings.String.EmptyString,$_typeof_Coq.Strings.String.String,$_typeof_Coq.Strings.String.string,$_typeof_Coq.Structures.DecidableTypeEx.N_as_DT.eq,$_typeof_Coq.Structures.DecidableTypeEx.N_as_DT.lt,$_typeof_Coq.Structures.DecidableTypeEx.N_as_DT.t,$_typeof_Coq.Structures.DecidableTypeEx.Nat_as_DT.eq,$_typeof_Coq.Structures.DecidableTypeEx.Nat_as_DT.lt,$_typeof_Coq.Structures.DecidableTypeEx.Nat_as_DT.t,$_typeof_Coq.Structures.DecidableTypeEx.Positive_as_DT.eq,$_typeof_Coq.Structures.DecidableTypeEx.Positive_as_DT.lt,$_typeof_Coq.Structures.DecidableTypeEx.Positive_as_DT.t,$_typeof_Coq.Structures.DecidableTypeEx.Z_as_DT.eq,$_typeof_Coq.Structures.DecidableTypeEx.Z_as_DT.lt,$_typeof_Coq.Structures.DecidableTypeEx.Z_as_DT.t,$_typeof_Coq.Structures.GenericMinMax.gmax,$_typeof_Coq.Structures.GenericMinMax.gmin,$_typeof_Coq.Structures.OrderedType.Compare,$_typeof_Coq.Structures.OrderedTypeEx.N_as_OT.eq,$_typeof_Coq.Structures.OrderedTypeEx.N_as_OT.lt,$_typeof_Coq.Structures.OrderedTypeEx.N_as_OT.t,$_typeof_Coq.Structures.OrderedTypeEx.Nat_as_OT.eq,$_typeof_Coq.Structures.OrderedTypeEx.Nat_as_OT.lt,$_typeof_Coq.Structures.OrderedTypeEx.Nat_as_OT.t,$_typeof_Coq.Structures.OrderedTypeEx.PositiveOrderedTypeBits.bits_lt,$_typeof_Coq.Structures.OrderedTypeEx.PositiveOrderedTypeBits.eq,$_typeof_Coq.Structures.OrderedTypeEx.PositiveOrderedTypeBits.lt,$_typeof_Coq.Structures.OrderedTypeEx.PositiveOrderedTypeBits.t,$_typeof_Coq.Structures.OrderedTypeEx.Positive_as_OT.eq,$_typeof_Coq.Structures.OrderedTypeEx.Positive_as_OT.lt,$_typeof_Coq.Structures.OrderedTypeEx.Positive_as_OT.t,$_typeof_Coq.Structures.OrderedTypeEx.String_as_OT.lt,$_typeof_Coq.Structures.OrderedTypeEx.String_as_OT.t,$_typeof_Coq.Structures.OrderedTypeEx.Z_as_OT.eq,$_typeof_Coq.Structures.OrderedTypeEx.Z_as_OT.lt,$_typeof_Coq.Structures.OrderedTypeEx.Z_as_OT.t,$_typeof_Coq.Structures.OrdersTac.OEQ,$_typeof_Coq.Structures.OrdersTac.OLE,$_typeof_Coq.Structures.OrdersTac.OLT,$_typeof_Coq.Structures.OrdersTac.ord,$_typeof_Coq.Vectors.Fin.t,$_typeof_Coq.Vectors.Vector.t,$_typeof_Coq.Vectors.VectorDef.nil,$_typeof_Coq.Vectors.VectorDef.t,$_typeof_Coq.ZArith.BinInt.Z.Private_Div.Quot2Div.div,$_typeof_Coq.ZArith.BinInt.Z.Private_Div.Quot2Div.modulo,$_typeof_Coq.ZArith.BinInt.Z.divide,$_typeof_Coq.ZArith.BinInt.Z.eq,$_typeof_Coq.ZArith.BinInt.Z.eqf,$_typeof_Coq.ZArith.BinInt.Z.le,$_typeof_Coq.ZArith.BinInt.Z.lt,$_typeof_Coq.ZArith.BinInt.Z.t,$_typeof_Coq.ZArith.BinInt.Z.to_pos,$_typeof_Coq.ZArith.BinInt.Z.zero,$_typeof_Coq.ZArith.BinInt.Zne,$_typeof_Coq.ZArith.BinIntDef.Z.abs,$_typeof_Coq.ZArith.BinIntDef.Z.abs_N,$_typeof_Coq.ZArith.BinIntDef.Z.add,$_typeof_Coq.ZArith.BinIntDef.Z.compare,$_typeof_Coq.ZArith.BinIntDef.Z.div,$_typeof_Coq.ZArith.BinIntDef.Z.even,$_typeof_Coq.ZArith.BinIntDef.Z.max,$_typeof_Coq.ZArith.BinIntDef.Z.min,$_typeof_Coq.ZArith.BinIntDef.Z.modulo,$_typeof_Coq.ZArith.BinIntDef.Z.mul,$_typeof_Coq.ZArith.BinIntDef.Z.odd,$_typeof_Coq.ZArith.BinIntDef.Z.of_N,$_typeof_Coq.ZArith.BinIntDef.Z.opp,$_typeof_Coq.ZArith.BinIntDef.Z.pow,$_typeof_Coq.ZArith.BinIntDef.Z.sub,$_typeof_Coq.ZArith.BinIntDef.Z.succ,$_typeof_Coq.ZArith.BinIntDef.Z.t,$_typeof_Coq.ZArith.BinIntDef.Z.to_N,$_typeof_Coq.ZArith.BinIntDef.Z.to_pos,$_typeof_Coq.ZArith.BinIntDef.Z.zero,$_typeof_Coq.ZArith.Zbool.Zeq_bool,$_typeof_Coq.ZArith.Zeven.Zeven,$_typeof_Coq.ZArith.Zeven.Zodd,$_typeof_Coq.ZArith.Zlogarithm.Is_power,$_typeof_Coq.ZArith.Znumtheory.Euclid,$_typeof_Coq.ZArith.Zpower.Zdiv_rest_proofs,$_typeof_Coq.micromega.Env.Env,$_typeof_Coq.micromega.EnvRing.Mon,$_typeof_Coq.micromega.EnvRing.PEc,$_typeof_Coq.micromega.EnvRing.PExpr,$_typeof_Coq.micromega.EnvRing.Pc,$_typeof_Coq.micromega.EnvRing.Pol,$_typeof_Coq.micromega.EnvRing.mon0,$_typeof_Coq.micromega.RMicromega.C0,$_typeof_Coq.micromega.RMicromega.C1,$_typeof_Coq.micromega.RMicromega.CInv,$_typeof_Coq.micromega.RMicromega.CMinus,$_typeof_Coq.micromega.RMicromega.CMult,$_typeof_Coq.micromega.RMicromega.COpp,$_typeof_Coq.micromega.RMicromega.CPlus,$_typeof_Coq.micromega.RMicromega.CQ,$_typeof_Coq.micromega.RMicromega.CZ,$_typeof_Coq.micromega.RMicromega.Rcst,$_typeof_Coq.micromega.Refl.make_conj,$_typeof_Coq.micromega.Refl.make_impl,$_typeof_Coq.micromega.RingMicromega.Equal,$_typeof_Coq.micromega.RingMicromega.Formula,$_typeof_Coq.micromega.RingMicromega.NonEqual,$_typeof_Coq.micromega.RingMicromega.NonStrict,$_typeof_Coq.micromega.RingMicromega.Op1,$_typeof_Coq.micromega.RingMicromega.Op2,$_typeof_Coq.micromega.RingMicromega.OpEq,$_typeof_Coq.micromega.RingMicromega.OpGe,$_typeof_Coq.micromega.RingMicromega.OpGt,$_typeof_Coq.micromega.RingMicromega.OpLe,$_typeof_Coq.micromega.RingMicromega.OpLt,$_typeof_Coq.micromega.RingMicromega.OpNEq,$_typeof_Coq.micromega.RingMicromega.PolC,$_typeof_Coq.micromega.RingMicromega.PolEnv,$_typeof_Coq.micromega.RingMicromega.Psatz,$_typeof_Coq.micromega.RingMicromega.Strict,$_typeof_Coq.micromega.Tauto.GFormula,$_typeof_Coq.micromega.VarMap.t,$_typeof_Coq.micromega.ZMicromega.DoneProof,$_typeof_Coq.micromega.ZMicromega.Vars.E.bits_lt,$_typeof_Coq.micromega.ZMicromega.Vars.E.eq,$_typeof_Coq.micromega.ZMicromega.Vars.E.lt,$_typeof_Coq.micromega.ZMicromega.Vars.E.t,$_typeof_Coq.micromega.ZMicromega.Vars.Leaf,$_typeof_Coq.micromega.ZMicromega.Vars.elt,$_typeof_Coq.micromega.ZMicromega.Vars.eq,$_typeof_Coq.micromega.ZMicromega.Vars.t,$_typeof_Coq.micromega.ZMicromega.Vars.tree,$_typeof_Coq.micromega.ZMicromega.ZArithProof,$_typeof_Coq.micromega.ZMicromega.coneMember,$_typeof_Coq.omega.PreOmega.Z_of_N',$_typeof_Coq.omega.PreOmega.Z_of_nat',$_typeof_Coq.omega.PreOmega.Zneg',$_typeof_Coq.omega.PreOmega.Zpos',$_typeof_Coq.setoid_ring.ArithRing.protected_to_nat,$_typeof_Coq.setoid_ring.Field_theory.FEX,$_typeof_Coq.setoid_ring.Field_theory.FEc,$_typeof_Coq.setoid_ring.Field_theory.FExpr,$_typeof_Coq.setoid_ring.Field_theory.linear,$_typeof_Coq.setoid_ring.Field_theory.rsplit,$_typeof_Coq.setoid_ring.InitialRing.NotConstant,$_typeof_Coq.setoid_ring.InitialRing.Nword,$_typeof_Coq.setoid_ring.InitialRing.gen_phiPOS,$_typeof_Coq.setoid_ring.InitialRing.gen_phiPOS1,$_typeof_Coq.setoid_ring.InitialRing.hypo,$_typeof_Coq.setoid_ring.InitialRing.mkhypo,$_typeof_Coq.setoid_ring.Ring_polynom.Mon,$_typeof_Coq.setoid_ring.Ring_polynom.PEI,$_typeof_Coq.setoid_ring.Ring_polynom.PEO,$_typeof_Coq.setoid_ring.Ring_polynom.PEX,$_typeof_Coq.setoid_ring.Ring_polynom.PEadd,$_typeof_Coq.setoid_ring.Ring_polynom.PEc,$_typeof_Coq.setoid_ring.Ring_polynom.PEmul,$_typeof_Coq.setoid_ring.Ring_polynom.PEopp,$_typeof_Coq.setoid_ring.Ring_polynom.PEsub,$_typeof_Coq.setoid_ring.Ring_polynom.PExpr,$_typeof_Coq.setoid_ring.Ring_polynom.Pc,$_typeof_Coq.setoid_ring.Ring_polynom.Pol,$_typeof_Coq.setoid_ring.Ring_polynom.mkmult_pow,$_typeof_Coq.setoid_ring.Ring_polynom.mon0,$_typeof_Coq.setoid_ring.Ring_polynom.vmon,$_typeof_Coq.setoid_ring.Ring_polynom.zmon,$_typeof_Coq.setoid_ring.Ring_tac.ring_subst_niter,$_typeof_Coq.setoid_ring.Ring_theory.Abstract,$_typeof_Coq.setoid_ring.Ring_theory.IDphi,$_typeof_Coq.setoid_ring.Ring_theory.SRopp,$_typeof_Coq.setoid_ring.Ring_theory.SRsub,$_typeof_Coq.setoid_ring.Ring_theory.id_phi_N,$_typeof_Coq.setoid_ring.Ring_theory.pow_N,$_typeof_Coq.setoid_ring.Ring_theory.pow_pos,$_typeof_Coq.setoid_ring.Ring_theory.ring_kind,$_typeof_Hammer.Tactics.Reconstr.AllHyps,$_typeof_Hammer.Tactics.Reconstr.Empty,$_typeof_Hammer.Tactics.Reconstr.ReconstrT,$_typeof_Hammer.Tactics.Reconstr.rdone,$_typeof_Hammer.Tactics.Tactics.rdone,$_typeof_PLF.Imp.AExp.AMinus,$_typeof_PLF.Imp.AExp.AMult,$_typeof_PLF.Imp.AExp.ANum,$_typeof_PLF.Imp.AExp.APlus,$_typeof_PLF.Imp.AExp.BFalse,$_typeof_PLF.Imp.AExp.BTrue,$_typeof_PLF.Imp.AExp.aexp,$_typeof_PLF.Imp.AExp.bexp,$_typeof_PLF.Imp.AId,$_typeof_PLF.Imp.AMinus,$_typeof_PLF.Imp.AMult,$_typeof_PLF.Imp.ANum,$_typeof_PLF.Imp.APlus,$_typeof_PLF.Imp.BAnd,$_typeof_PLF.Imp.BEq,$_typeof_PLF.Imp.BFalse,$_typeof_PLF.Imp.BLe,$_typeof_PLF.Imp.BNot,$_typeof_PLF.Imp.BTrue,$_typeof_PLF.Imp.BreakImp.CBreak,$_typeof_PLF.Imp.BreakImp.CSkip,$_typeof_PLF.Imp.BreakImp.SBreak,$_typeof_PLF.Imp.BreakImp.SContinue,$_typeof_PLF.Imp.BreakImp.com,$_typeof_PLF.Imp.BreakImp.result,$_typeof_PLF.Imp.CSeq,$_typeof_PLF.Imp.CSkip,$_typeof_PLF.Imp.SLoad,$_typeof_PLF.Imp.SMinus,$_typeof_PLF.Imp.SMult,$_typeof_PLF.Imp.SPlus,$_typeof_PLF.Imp.SPush,$_typeof_PLF.Imp.X,$_typeof_PLF.Imp.Y,$_typeof_PLF.Imp.aevalR_division.ANum,$_typeof_PLF.Imp.aevalR_division.aexp,$_typeof_PLF.Imp.aevalR_extended.AAny,$_typeof_PLF.Imp.aevalR_extended.ANum,$_typeof_PLF.Imp.aevalR_extended.aexp,$_typeof_PLF.Imp.aexp,$_typeof_PLF.Imp.bexp,$_typeof_PLF.Imp.com,$_typeof_PLF.Imp.empty_st,$_typeof_PLF.Imp.pup_to_n,$_typeof_PLF.Imp.sinstr,$_typeof_PLF.Imp.state,$_typeof_PLF.Maps.eqb_string,$_typeof_PLF.Maps.t_update,$_typeof_PLF.Maps.total_map,$_typeof_PLF.Smallstep.C,$_typeof_PLF.Smallstep.CImp.CAss,$_typeof_PLF.Smallstep.CImp.CIf,$_typeof_PLF.Smallstep.CImp.CPar,$_typeof_PLF.Smallstep.CImp.CSeq,$_typeof_PLF.Smallstep.CImp.CSkip,$_typeof_PLF.Smallstep.CImp.CWhile,$_typeof_PLF.Smallstep.CImp.cmultistep,$_typeof_PLF.Smallstep.CImp.com,$_typeof_PLF.Smallstep.Combined.C,$_typeof_PLF.Smallstep.Combined.P,$_typeof_PLF.Smallstep.Combined.fls,$_typeof_PLF.Smallstep.Combined.test,$_typeof_PLF.Smallstep.Combined.tm,$_typeof_PLF.Smallstep.Combined.tru,$_typeof_PLF.Smallstep.P,$_typeof_PLF.Smallstep.Temp4.fls,$_typeof_PLF.Smallstep.Temp4.test,$_typeof_PLF.Smallstep.Temp4.tm,$_typeof_PLF.Smallstep.Temp4.tru,$_typeof_PLF.Smallstep.compiler_is_correct_statement,$_typeof_PLF.Smallstep.normal_form,$_typeof_PLF.Smallstep.normal_form_of,$_typeof_PLF.Smallstep.normalizing,$_typeof_PLF.Smallstep.prog,$_typeof_PLF.Smallstep.relation,$_typeof_PLF.Smallstep.stack,$_typeof_PLF.Smallstep.stack_multistep,$_typeof_PLF.Smallstep.step_normal_form,$_typeof_PLF.Smallstep.tm,$_typeof_Stlc.STLC.Arrow,$_typeof_Stlc.STLC.Bool,$_typeof_Stlc.STLC.abs,$_typeof_Stlc.STLC.app,$_typeof_Stlc.STLC.fls,$_typeof_Stlc.STLC.subst,$_typeof_Stlc.STLC.substi_rec,$_typeof_Stlc.STLC.substi_rect,$_typeof_Stlc.STLC.test,$_typeof_Stlc.STLC.tm,$_typeof_Stlc.STLC.tm_rec,$_typeof_Stlc.STLC.tm_rect,$_typeof_Stlc.STLC.tru,$_typeof_Stlc.STLC.ty,$_typeof_Stlc.STLC.ty_rec,$_typeof_Stlc.STLC.ty_rect,$_typeof_Stlc.STLC.var,$_typeof_Stlc.STLC.x,Coq.Arith.PeanoNat.Nat.Private_OrderTac.Tac.eq_refl,Coq.Arith.PeanoNat.Nat.Private_OrderTac.Tac.eq_sym,Coq.Arith.PeanoNat.Nat.Private_OrderTac.Tac.le_refl,Coq.Arith.PeanoNat.Nat.Private_OrderTac.Tac.lt_irrefl,Coq.Arith.PeanoNat.Nat.Private_OrderTac.Tac.not_gt_le,Coq.Arith.PeanoNat.Nat.Private_Tac.eq_refl,Coq.Arith.PeanoNat.Nat.Private_Tac.eq_sym,Coq.Arith.PeanoNat.Nat.Private_Tac.le_refl,Coq.Arith.PeanoNat.Nat.Private_Tac.lt_irrefl,Coq.Arith.PeanoNat.Nat.add_comm,Coq.Arith.PeanoNat.Nat.divide_refl,Coq.Arith.PeanoNat.Nat.eq_equiv,Coq.Arith.PeanoNat.Nat.le_0_l,Coq.Arith.PeanoNat.Nat.le_ge_cases,Coq.Arith.PeanoNat.Nat.le_gt_cases,Coq.Arith.PeanoNat.Nat.le_refl,Coq.Arith.PeanoNat.Nat.le_trans,Coq.Arith.PeanoNat.Nat.lt_ge_cases,Coq.Arith.PeanoNat.Nat.lt_le_incl,Coq.Arith.PeanoNat.Nat.lt_trans,Coq.Arith.PeanoNat.Nat.lt_trichotomy,Coq.Arith.Wf_nat.lt_wf_double_ind,Coq.Arith.Wf_nat.lt_wf_ind,Coq.Bool.Bool.absurd_eq_bool,Coq.Init.Datatypes.idProp,Coq.Init.Datatypes.nat_ind,Coq.Init.Peano.le_n,Coq.Logic.Decidable.dec_not_not,Coq.Logic.Decidable.not_and_iff,Coq.Logic.Decidable.not_or_iff,Coq.Logic.Decidable.not_true_iff,Coq.Logic.FunctionalExtensionality.equal_f,Coq.Logic.FunctionalExtensionality.equal_f_dep,Coq.Logic.FunctionalExtensionality.eta_expansion,Coq.Logic.FunctionalExtensionality.eta_expansion_dep,Coq.Logic.FunctionalExtensionality.functional_extensionality,Coq.Logic.FunctionalExtensionality.functional_extensionality_dep,Coq.NArith.BinNat.N.Private_OrderTac.Tac.eq_refl,Coq.NArith.BinNat.N.Private_OrderTac.Tac.eq_sym,Coq.NArith.BinNat.N.Private_OrderTac.Tac.le_refl,Coq.NArith.BinNat.N.Private_OrderTac.Tac.lt_irrefl,Coq.NArith.BinNat.N.Private_Tac.eq_refl,Coq.NArith.BinNat.N.Private_Tac.eq_sym,Coq.NArith.BinNat.N.Private_Tac.le_refl,Coq.NArith.BinNat.N.Private_Tac.lt_irrefl,Coq.NArith.BinNat.N.eq_equiv,Coq.NArith.BinNat.N.le_0_l,Coq.NArith.BinNat.N.le_ge_cases,Coq.NArith.BinNat.N.le_gt_cases,Coq.NArith.BinNat.N.le_refl,Coq.PArith.BinPos.Pos.Private_Tac.eq_refl,Coq.PArith.BinPos.Pos.Private_Tac.eq_sym,Coq.PArith.BinPos.Pos.Private_Tac.le_refl,Coq.ZArith.BinInt.Z.Private_OrderTac.Tac.eq_refl,Coq.ZArith.BinInt.Z.Private_OrderTac.Tac.eq_sym,Coq.ZArith.BinInt.Z.Private_OrderTac.Tac.le_antisym,Coq.ZArith.BinInt.Z.Private_OrderTac.Tac.le_refl,Coq.ZArith.BinInt.Z.Private_OrderTac.Tac.lt_irrefl,Coq.ZArith.BinInt.Z.Private_OrderTac.Tac.not_ge_lt,Coq.ZArith.BinInt.Z.Private_OrderTac.Tac.not_gt_le,Coq.ZArith.BinInt.Z.Private_Tac.eq_refl,Coq.ZArith.BinInt.Z.Private_Tac.eq_sym,Coq.ZArith.BinInt.Z.Private_Tac.le_refl,Coq.ZArith.BinInt.Z.Private_Tac.lt_irrefl,Coq.ZArith.BinInt.Z.add_comm,Coq.ZArith.BinInt.Z.divide_refl,Coq.ZArith.BinInt.Z.eq_equiv,Coq.ZArith.BinInt.Z.le_ge_cases,Coq.ZArith.BinInt.Z.le_gt_cases,Coq.ZArith.BinInt.Z.le_refl,Coq.ZArith.BinInt.Z.le_trans,Coq.ZArith.BinInt.Z.lt_ge_cases,Coq.ZArith.BinInt.Z.lt_le_incl,Coq.ZArith.BinInt.Z.lt_trans,Coq.ZArith.BinInt.Z.lt_trichotomy,Coq.ZArith.BinInt.Z.mul_comm,Coq.micromega.OrderedRing.Rle_antisymm,Coq.micromega.OrderedRing.Rle_gt_cases,Coq.micromega.OrderedRing.Rle_lt_trans,Coq.micromega.OrderedRing.Rle_refl,Coq.micromega.OrderedRing.Rle_trans,Coq.micromega.OrderedRing.Rlt_0_1,Coq.micromega.OrderedRing.Rlt_le_trans,Coq.micromega.OrderedRing.Rlt_lt_succ,Coq.micromega.OrderedRing.Rlt_succ_r,Coq.micromega.OrderedRing.Rlt_trans,Coq.micromega.OrderedRing.Rlt_trichotomy,Coq.micromega.OrderedRing.Rplus_0_l,Coq.micromega.OrderedRing.Rplus_0_r,Coq.micromega.OrderedRing.Rplus_comm,Coq.micromega.OrderedRing.Rplus_le_lt_mono,Coq.micromega.OrderedRing.Rplus_le_mono,Coq.micromega.OrderedRing.Rplus_lt_le_mono,Coq.micromega.OrderedRing.Rplus_lt_mono,Coq.micromega.OrderedRing.Rplus_nonneg_nonneg,Coq.micromega.OrderedRing.Rplus_nonneg_pos,Coq.micromega.OrderedRing.Rplus_pos_nonneg,Coq.micromega.OrderedRing.Rplus_pos_pos,Coq.micromega.OrderedRing.Rtimes_0_l,Coq.micromega.OrderedRing.Rtimes_0_r,Coq.micromega.OrderedRing.Rtimes_comm,Coq.micromega.OrderedRing.Rtimes_neg_neg,Coq.micromega.OrderedRing.Rtimes_nonneg_nonneg,Coq.micromega.OrderedRing.Rtimes_pos_neg,Coq.micromega.OrderedRing.Rtimes_pos_pos,Coq.micromega.OrderedRing.Rtimes_square_nonneg,Coq.micromega.ZCoeff.req_refl,Coq.micromega.ZCoeff.req_sym,Coq.micromega.ZCoeff.req_trans,Coq.omega.OmegaLemmas.new_var,Coq.setoid_ring.Ring_theory.ARmul_0_l,Coq.setoid_ring.Ring_theory.ARmul_1_l,Coq.setoid_ring.Ring_theory.ARmul_assoc,Coq.setoid_ring.Ring_theory.ARmul_comm,Coq.setoid_ring.Ring_theory.ARopp_mul_l,Coq.setoid_ring.Ring_theory.ARsub_def,PLF.Imp.AExp.silly2,PLF.Maps.t_update_eq,PLF.Maps.t_update_neq,PLF.Smallstep.AS_Id,PLF.Smallstep.AS_Plus1,PLF.Smallstep.BS_Eq1,PLF.Smallstep.ST_Plus1,PLF.Smallstep.ST_Plus2,PLF.Smallstep.ST_PlusConstConst,PLF.Smallstep.Temp4.Temp5.bool_step_prop4_holds,PLF.Smallstep.compiler_is_correct,PLF.Smallstep.eval__multistep,PLF.Smallstep.multi_R,PLF.Smallstep.multi_ind,PLF.Smallstep.multi_refl,PLF.Smallstep.multi_step,PLF.Smallstep.multi_trans,PLF.Smallstep.multistep_congr_1,PLF.Smallstep.multistep_congr_2,PLF.Smallstep.step_example1,PLF.Smallstep.step_example1',PLF.Smallstep.step_example1'',PLF.Smallstep.step_example1''',PLF.Smallstep.test_multistep_2,PLF.Smallstep.test_multistep_3,PLF.Smallstep.v_const,Stlc.STLC.ST_App1,Stlc.STLC.ST_App2,Stlc.STLC.ST_AppAbs,Stlc.STLC.ST_Test,Stlc.STLC.ST_TestFls,Stlc.STLC.ST_TestTru,Stlc.STLC.s_var1,Stlc.STLC.step_example1,Stlc.STLC.step_example2,Stlc.STLC.step_example3,Stlc.STLC.step_example4,Stlc.STLC.step_ind,Stlc.STLC.substi_correct,Stlc.STLC.substi_ind,Stlc.STLC.tm_ind,Stlc.STLC.ty_ind,Stlc.STLC.v_abs,Stlc.STLC.v_fls,Stlc.STLC.v_tru,Stlc.STLC.value_ind,$adef_Coq.Arith.PeanoNat.Nat.eqf_$a2,$adef_PLF.Smallstep.Temp4.step_$a2,$adef_PLF.Smallstep.P_$a2,$adef_Coq.NArith.Ndigits.eqf_$a2,$adef_$_lam_32206_$a5,$adef_Coq.PArith.BinPos.Pos.PeanoSucc_$a2,$adef_$_case_Stlc.STLC.tm$112908_$a5,$adef_Coq.Reals.Rdefinitions.IZR_$a1,$adef_$_case_Coq.Numbers.BinNums.Z$139518_$a3,$adef_Coq.Relations.Relation_Definitions.preorder_$a2,$adef_Coq.Init.Datatypes.None_$a1,$adef_PLF.Smallstep.multi_$a2,$adef_Coq.NArith.BinNat.N.lt_$a2,$adef_Coq.Vectors.VectorDef.cons_$a4,$adef_Coq.ZArith.BinIntDef.Z.of_N_$a1,$adef_Coq.ZArith.BinIntDef.Z.modulo_$a2,$adef_Coq.Init.Datatypes.BoolSpec_$a3,$adef_PLF.Imp.beval_$a2,$adef_Coq.setoid_ring.Ring_theory.SRopp_$a2,$adef_Coq.micromega.VarMap.t_$a1,$adef_Coq.Init.Decimal.nzhead_$a1,$adef_PLF.Smallstep.Combined.step_$a2,$adef_Coq.Lists.List.Exists_$a3,$adef_Coq.micromega.RingMicromega.PsatzMulC_$a3,$adef_PLF.Imp.aevalR_division.APlus_$a2,$adef_Coq.Reals.Rfunctions.ZintPos_$a2,$adef_$_case_Coq.Init.Datatypes.nat$34601_$a2,$adef_Coq.setoid_ring.Ring_theory.sring_eq_ext_$a4,$adef_Coq.setoid_ring.Ring_polynom.PEc_$a2,$adef_PLF.Smallstep.stack_step_$a3,$adef_PLF.Smallstep.SimpleArith1.step_$a2,$adef_Coq.Vectors.VectorDef.Forall_$a4,$adef_Coq.Init.Datatypes.implb_$a2,$adef_Coq.micromega.EnvRing.Pol_$a1,$adef_Coq.micromega.Tauto.Cj_$a6,$adef_Coq.setoid_ring.Ring_polynom.PEmul_$a3,$adef_Coq.Relations.Relation_Operators.clos_refl_$a4,$adef_Coq.setoid_ring.Ring_polynom.Pc_$a2,$adef_Coq.PArith.BinPos.Pos.iter_$a4,$adef_Coq.micromega.RMicromega.CMult_$a2,$adef_Coq.micromega.DeclConstant.GT_$a2,$adef_Stlc.STLC.tm_rect_$a1,$adef_Coq.Init.Nat.log2_iter_$a4,$adef_PLF.Smallstep.Temp1.step_$a2,$adef_Coq.Relations.Relation_Definitions.symmetric_$a2,$adef_Coq.Init.Nat.even_$a1,$adef_Coq.Sorting.Sorted.LocallySorted_$a3,$adef_Coq.setoid_ring.Ring_polynom.vmon_$a2,$adef_Stlc.STLC.test_$a3,$adef_Coq.Init.Decimal.Pos_$a1,$adef_Coq.setoid_ring.Ring_polynom.Pol_$a1,$adef_Coq.FSets.FSetPositive.PositiveSet.mem_$a2,$adef_Coq.Arith.Between.P_nth_$a5,$adef_Coq.Relations.Relation_Operators.clos_refl_sym_trans_n1_$a4,$adef_Coq.micromega.Env.Env_$a1,$adef_$_lam_142139_$a3,$adef_PLF.Imp.AExp.BNot_$a1,$adef_Coq.Init.Datatypes.CompareSpecT_$a4,$adef_Coq.micromega.ZMicromega.Vars.Facts.MP.Dec.FSetDecideAuxiliary.FSet_elt_Prop_$a1,$adef_Coq.setoid_ring.Field_theory.FEdiv_$a3,$adef_Coq.Init.Nat.compare_$a2,$adef_Coq.setoid_ring.Ring_theory.almost_ring_theory_$a8,$adef_Coq.Init.Datatypes.app_$a3,$adef_Coq.Init.Specif.existT_$a4,$adef_Coq.Init.Decimal.D6_$a1,$adef_Coq.Init.Specif.sig_$a2,$adef_Coq.Relations.Relation_Operators.lexprod_$a6,$adef_Coq.setoid_ring.Field_theory.FEmul_$a3,$adef_$_prop_35_$a2,$adef_Coq.Vectors.Vector.nil_$a1,$adef_$_case_Coq.Init.Datatypes.nat$34211_$a5,$adef_Coq.ZArith.BinIntDef.Z.mul_$a2,$adef_PLF.Smallstep.Temp3.value_$a1,$adef_Coq.micromega.ZMicromega.Vars.ct_$a3,$adef_Coq.micromega.ZMicromega.EnumProof_$a3,$adef_Coq.PArith.BinPosDef.Pos.iter_$a4,$adef_$_fix_141724_v_CANONICAL_0_$a1,$adef_Coq.Relations.Relation_Operators.symprod_$a6,$adef_$_prop_34_$a2,$adef_Coq.Init.Decimal.D4_$a1,$adef_Coq.FSets.FSetPositive.PositiveSet.Equal_$a2,$adef_Coq.micromega.RingMicromega.Build_Formula_$a4,$adef_Coq.setoid_ring.Ring_polynom.mkmult_pow_$a5,$adef_$_lam_149467_$a2,$adef_Coq.Init.Specif.sumbool_$a2,$adef_PLF.Smallstep.CImp.CPar_$a2,$adef_Coq.PArith.BinPos.Pos.IsPos_$a1,$adef_Coq.setoid_ring.Field_theory.mk_rsplit_$a4,$adef_PLF.Imp.BLe_$a2,$adef_$_case_Coq.Init.Datatypes.nat$139501_$a3,$adef_$_prop_141641_$a3,$adef_Coq.Sets.Relations_1.Relation_$a1,$adef_Coq.setoid_ring.Ring_theory.semi_ring_theory_$a6,$adef_Coq.Reals.RIneq.mknonposreal_$a1,$adef_PLF.Imp.aeval_$a2,$adef_Coq.Lists.SetoidList.transpose_restr2_$a5,$adef_PLF.Imp.ceval_$a3,$adef_PLF.Imp.AMinus_$a2,$adef_Coq.Init.Specif.proj1_sig_$a3,$adef_Coq.setoid_ring.Ring_polynom.PEsub_$a3,$adef_$_lam_31563_$a6,$adef_Coq.FSets.FSetPositive.PositiveSet.ct_$a3,$adef_Coq.Init.Nat.max_$a2,$adef_Coq.PArith.BinPosDef.Pos.pred_N_$a1,$adef_PLF.Imp.BreakImp.CIf_$a3,$adef_Coq.Structures.OrderedTypeEx.Z_as_OT.lt_$a2,$adef_Coq.Lists.List.hd_$a3,$adef_Coq.Init.Datatypes.option_$a1,$adef_Coq.Relations.Relation_Definitions.relation_$a1,$adef_PLF.Imp.BNot_$a1,$adef_PLF.Imp.BAnd_$a2,$adef_$_case_Coq.Init.Datatypes.nat$109204_$a4,$adef_Coq.Structures.OrderedType.LT_$a5,$adef_$_case_Coq.Init.Datatypes.nat$139523_$a1,$adef_Coq.Vectors.VectorDef.t_$a2,$adef_$_case_Coq.Init.Datatypes.bool$113326_$a4,$adef_Coq.setoid_ring.Ring_polynom.PExpr_$a1,$adef_Coq.Init.Datatypes.orb_$a2,$adef_Coq.Arith.Plus.tail_plus_$a2,$adef_Coq.setoid_ring.Ring_theory.ring_morph_$a17,$adef_Coq.Init.Datatypes.CompOpp_$a1,$adef_Coq.micromega.EnvRing.PEopp_$a2,$adef_Stlc.STLC.ty_rect_$a1,$adef_Coq.micromega.RingMicromega.SORaddon_$a22,$adef_Coq.ZArith.Zpower.two_power_pos_$a1,$adef_Coq.Arith.Between.exists_between_$a3,$adef_Coq.setoid_ring.Field_theory.FExpr_$a1,$adef_$_case_Coq.Init.Datatypes.nat$35257_$a5,$adef_Coq.micromega.RingMicromega.PolEnv_$a1,$adef_Coq.Init.Datatypes.identity_$a3,$adef_PLF.Imp.ANum_$a1,$adef_PLF.Smallstep.stack_step_$a1,$adef_Coq.Init.Datatypes.id_$a2,$adef_$_case_Coq.Init.Datatypes.nat$136884_$a4,$adef_PLF.Smallstep.CImp.cstep_$a2,$adef_Coq.Reals.Rdefinitions.Rle_$a2,$adef_Coq.Relations.Relation_Definitions.order_$a2,$adef_PLF.Smallstep.Temp3.step_$a2,$adef_PLF.Imp.aevalR_extended.APlus_$a2,$adef_Coq.micromega.EnvRing.zmon_$a2,$adef_Coq.Bool.Zerob.zerob_$a1,$adef_Coq.Logic.EqdepFacts.eq_dep_$a6,$adef_PLF.Smallstep.multi_$a4,$adef_Coq.Init.Nat.eqb_$a2,$adef_$_lam_149529_$a1,$adef_Coq.setoid_ring.Ring_theory.div_theory_$a7,$adef_Coq.Sorting.Sorted.HdRel_$a4,$adef_Hammer.Tactics.Reconstr.rdone_$a2,$adef_Coq.Reals.Rfunctions.Z_spec_$a2,$adef_Coq.Init.Datatypes.inl_$a3,$adef_Coq.Lists.SetoidList.transpose2_$a4,$adef_Coq.setoid_ring.Ring_theory.ring_eq_ext_$a5,$adef_PLF.Maps.t_empty_$a2,$adef_PLF.Smallstep.CImp.CWhile_$a2,$adef_PLF.Imp.AExp.BAnd_$a2,$adef_Coq.ZArith.BinIntDef.Z.to_N_$a1,$adef_Coq.Lists.List.Forall2_$a5,$adef_Coq.Relations.Relation_Definitions.reflexive_$a2,$adef_Coq.Init.Datatypes.nil_$a1,$adef_Coq.Logic.EqdepFacts.eq_dep1_$a6,$adef_$_case_Coq.Init.Datatypes.nat$35482_$a5,$adef_Coq.NArith.BinNatDef.N.max_$a2,$adef_$_case_Coq.Init.Datatypes.prod$134502_$a9,$adef_PLF.Imp.aevalR_division.ANum_$a1,$adef_Coq.Init.Datatypes.CompGtT_$a3,$adef_Coq.Reals.Rdefinitions.Rmult_$a2,$adef_Coq.Reals.Rfunctions.ZintNeg_$a2,$adef_Coq.micromega.Tauto.GFormula_$a4,$adef_Coq.ZArith.Znumtheory.Bezout_$a3,$adef_Coq.Numbers.BinNums.Npos_$a1,$adef_Coq.setoid_ring.Ring_theory.Morphism_$a17,$adef_Coq.setoid_ring.Ring_theory.IDphi_$a2,$adef_Stlc.STLC.tm_rec_$a1,$adef_$_lam_142139_$a4,$adef_PLF.Smallstep.bstep_$a3,$adef_Coq.Numbers.BinNums.xI_$a1,$adef_Coq.ZArith.Zeven.Zodd_$a1,$adef_Coq.Structures.GenericMinMax.gmax_$a4,$adef_Coq.micromega.RMicromega.CPow_$a2,$adef_Coq.micromega.RMicromega.CPlus_$a2,$adef_Coq.Init.Decimal.D1_$a1,$adef_Coq.NArith.BinNat.N.recursion_$a1,$adef_Coq.ZArith.BinIntDef.Z.to_pos_$a1,$adef_Coq.Init.Nat.div2_$a1,$adef_Coq.Init.Datatypes.negb_$a1,$adef_Coq.micromega.RMicromega.COpp_$a1,$adef_PLF.Imp.CIf_$a3,$adef_PLF.Smallstep.step_normal_form_$a1,$adef_Coq.PArith.BinPosDef.Pos.div2_$a1,$adef_PLF.Smallstep.Combined.P_$a2,$adef_Coq.Arith.Even.odd_$a1,$adef_Coq.Arith.PeanoNat.Nat.add_$a2,$adef_PLF.Smallstep.astep_$a3,$adef_Coq.Lists.List.ForallOrdPairs_$a3,$adef_Coq.ZArith.BinIntDef.Z.succ_$a1,$adef_PLF.Smallstep.Temp4.value_$a1,$adef_Coq.Relations.Relation_Operators.clos_trans_1n_$a4,$adef_Coq.Init.Logic_Type.notT_$a1,$adef_Coq.Init.Nat.add_$a2,$adef_Coq.Init.Specif.sigT2_$a3,$adef_Coq.Structures.OrderedType.Compare_$a5,$adef_$_lam_31563_$a7,$adef_Coq.setoid_ring.Field_theory.FEc_$a2,$adef_Coq.Classes.Morphisms.Proper_$a3,$adef_Coq.ZArith.BinIntDef.Z.pos_sub_$a2,$adef_Coq.Init.Specif.right_$a2,$adef_$_case_Coq.Init.Datatypes.bool$113543_$a4,$adef_Coq.setoid_ring.Ring_theory.power_theory_$a7,$adef_PLF.Imp.AExp.AMinus_$a2,$adef_Coq.Lists.List.fold_left_$a5,$adef_Coq.setoid_ring.Ring_polynom.Pinj_$a3,$adef_Coq.Sorting.Sorted.StronglySorted_$a3,$adef_PLF.Smallstep.value_$a1,$adef_PLF.Imp.AExp.AMult_$a2,$adef_Coq.ZArith.BinIntDef.Z.div_eucl_$a2,$adef_Coq.Lists.List.Add_$a4,$adef_Coq.micromega.RMicromega.CMinus_$a2,$adef_Coq.Bool.Bool.ifb_$a3,$adef_$_lam_142147_$a3,$adef_Coq.setoid_ring.Field_theory.FEadd_$a3,$adef_Coq.ZArith.BinIntDef.Z.odd_$a1,$adef_Coq.Init.Datatypes.S_$a1,$adef_$_prop_141657_$a3,$adef_Coq.Strings.Ascii.Ascii_$a8,$adef_Coq.micromega.EnvRing.PEpow_$a3,$adef_Coq.setoid_ring.Ring_polynom.zmon_$a2,$adef_Coq.setoid_ring.Ring_theory.semi_morph_$a13,$adef_PLF.Smallstep.CImp.CAss_$a2,$adef_Stlc.STLC.ty_rect_$a4,$adef_Coq.ZArith.BinIntDef.Z.add_$a2,$adef_Coq.micromega.RingMicromega.Formula_$a1,$adef_Coq.Reals.RIneq.mknegreal_$a1,$adef_Coq.setoid_ring.Ring_theory.SRsub_$a4,$adef_Coq.setoid_ring.InitialRing.gen_phiPOS1_$a5,$adef_Coq.micromega.ZMicromega.RatProof_$a2,$adef_Coq.micromega.RingMicromega.PolC_$a1,$adef_PLF.Imp.AMult_$a2,$adef_Coq.Lists.SetoidList.InA_$a4,$adef_PLF.Imp.CSeq_$a2,$adef_Coq.Reals.Rdefinitions.Rlt_$a2,$adef_$_fix_128730_v_CANONICAL_1_$a3,$adef_Coq.ZArith.BinIntDef.Z.sub_$a2,$adef_Coq.setoid_ring.Ring_polynom.PEopp_$a2,$adef_$_lam_149529_$a2,$adef_Coq.setoid_ring.Field_theory.mk_linear_$a4,$adef_Coq.setoid_ring.Ring_theory.pow_pos_$a4,$adef_Coq.Relations.Relation_Operators.Ltl_$a4,$adef_Coq.Vectors.Vector.Forall2_$a6,$adef_Coq.Init.Nat.pow_$a2,$adef_Coq.micromega.Tauto.I_$a7,$adef_Coq.micromega.Refl.make_conj_$a3,$adef_PLF.Imp.AExp.APlus_$a2,$adef_Coq.ZArith.BinIntDef.Z.even_$a1,$adef_Coq.Arith.PeanoNat.Nat.log2_iter_$a4,$adef_Coq.Init.Logic.eq_rect_$a5,$adef_Coq.setoid_ring.Ring_polynom.PEO_$a1,$adef_Coq.Numbers.BinNums.xO_$a1,$adef_Coq.Lists.SetoidList.transpose_restr_$a5,$adef_Coq.Vectors.Vector.t_$a2,$adef_Coq.setoid_ring.Field_theory.FEinv_$a2,$adef_Coq.ZArith.Zpower.Zdiv_rest_proof_$a4,$adef_Coq.Init.Wf.Acc_$a3,$adef_Coq.setoid_ring.Ring_theory.pow_N_$a5,$adef_PLF.Smallstep.Temp4.test_$a3,$adef_Coq.setoid_ring.Field_theory.semi_field_theory_$a8,$adef_Coq.Init.Decimal.D8_$a1,$adef_Coq.Relations.Relation_Operators.swapprod_$a4,$adef_$_let_var_6_p_139569_139571_$a4,$adef_Coq.ZArith.BinInt.Z.ge_$a2,$adef_Coq.ZArith.Zbool.Zeq_bool_$a2,$adef_Stlc.STLC.app_$a2,$adef_Coq.micromega.RMicromega.CQ_$a1,$adef_Coq.QArith.QArith_base.Qmake_$a2,$adef_Coq.setoid_ring.Ring_polynom.PEX_$a2,$adef_Coq.micromega.EnvRing.PEc_$a2,$adef_Coq.NArith.BinNatDef.N.pred_$a1,$adef_Coq.micromega.OrderedRing.SOR_$a10,$adef_Coq.Relations.Relation_Operators.clos_refl_trans_$a4,$adef_Coq.Init.Datatypes.sum_$a2,$adef_Coq.NArith.BinNatDef.N.min_$a2,$adef_Coq.ZArith.Znumtheory.Zis_gcd_$a3,$adef_Coq.PArith.BinPosDef.Pos.iter_op_$a4,$adef_Coq.micromega.ZMicromega.Vars.Node_$a3,$adef_Coq.Relations.Relation_Operators.clos_trans_$a4,$adef_Coq.Relations.Relation_Operators.clos_refl_sym_trans_1n_$a4,$adef_Coq.Vectors.Fin.t_$a1,$adef_Coq.setoid_ring.Field_theory.FEO_$a1,$adef_$_fix_34230_v_CANONICAL_0_$a2,$adef_Coq.Lists.List.In_$a3,$adef_$_case_Coq.Init.Datatypes.nat$35379_$a5,$adef_PLF.Smallstep.normal_form_$a3,$adef_Coq.Init.Datatypes.andb_$a2,$adef_Coq.Init.Peano.lt_$a2,$adef_Coq.PArith.BinPos.Pos.le_$a2,$adef_Coq.micromega.ZMicromega.CutProof_$a2,$adef_Stlc.STLC.substi_rec_$a3,$adef_Coq.ZArith.BinIntDef.Z.max_$a2,$adef_Coq.Structures.GenericMinMax.gmin_$a4,$adef_Coq.Init.Nat.mul_$a2,$adef_Coq.Init.Peano.le_$a2,$adef_Coq.Init.Decimal.D7_$a1,$adef_Coq.FSets.FSetPositive.PositiveSet.Node_$a3,$adef_Coq.Arith.PeanoNat.Nat.divide_$a2,$adef_$_case_Coq.Init.Datatypes.nat$34914_$a2,$adef_Coq.setoid_ring.Field_theory.rsplit_$a1,$adef_Coq.Init.Decimal.D2_$a1,$adef_Coq.Classes.RelationClasses.Equivalence_$a2,$adef_Coq.Arith.Even.even_$a1,$adef_Coq.micromega.Tauto.TT_$a4,$adef_Coq.Logic.Decidable.decidable_$a1,$adef_Coq.Relations.Relation_Operators.clos_trans_n1_$a4,$adef_Coq.Relations.Relation_Definitions.PER_$a2,$adef_Coq.micromega.EnvRing.PEmul_$a3,$adef_Coq.Init.Datatypes.snd_$a3,$adef_Coq.ZArith.BinInt.Z.eqf_$a2,$adef_$_fix_113301_v_CANONICAL_0_$a3,$adef_Coq.NArith.BinNatDef.N.testbit_$a2,$adef_Coq.PArith.BinPosDef.Pos.to_nat_$a1,$adef_Coq.Init.Decimal.D0_$a1,$adef_Coq.Relations.Relation_Definitions.antisymmetric_$a2,$adef_Coq.ZArith.BinIntDef.Z.abs_N_$a1,$adef_PLF.Imp.BreakImp.CAss_$a2,$adef_Coq.Init.Datatypes.CompLtT_$a3,$adef_Stlc.STLC.step_$a2,$adef_Coq.Lists.List.nth_$a4,$adef_Coq.Lists.SetoidList.transpose_$a4,$adef_Coq.Init.Datatypes.nat_rect_$a1,$adef_Coq.ZArith.Znumtheory.prime_$a1,$adef_PLF.Smallstep.CImp.CIf_$a3,$adef_$_case_Coq.Init.Datatypes.nat$113965_$a4,$adef_PLF.Imp.aevalR_division.AMinus_$a2,$adef_Coq.Init.Datatypes.inr_$a3,$adef_Coq.micromega.VarMap.Branch_$a4,$adef_Coq.Reals.RIneq.mkposreal_$a1,$adef_Coq.Vectors.Fin.F1_$a1,$adef_$_prop_141637_$a3,$adef_Coq.QArith.QArith_base.Qnum_$a1,$adef_Stlc.STLC.abs_$a3,$adef_$_fix_34144_v_CANONICAL_0_$a2,$adef_PLF.Smallstep.normalizing_$a2,$adef_Coq.Structures.OrderedTypeEx.PositiveOrderedTypeBits.bits_lt_$a2,$adef_PLF.Smallstep.Combined.C_$a1,$adef_Stlc.STLC.tm_rect_$a8,$adef_Coq.PArith.BinPosDef.Pos.succ_$a1,$adef_Coq.setoid_ring.Field_theory.FEsub_$a3,$adef_PLF.Maps.t_update_$a5,$adef_Coq.FSets.FSetPositive.PositiveSet.E.bits_lt_$a2,$adef_Coq.Relations.Relation_Operators.Desc_$a3,$adef_Coq.micromega.Tauto.D_$a6,$adef_PLF.Smallstep.Temp2.step_$a2,$adef_Coq.Init.Datatypes.prod_$a2,$adef_PLF.Maps.eqb_string_$a2,$adef_Coq.Init.Specif.Exc_$a1,$adef_Coq.Vectors.VectorDef.Forall2_$a6,$adef_Coq.micromega.DeclConstant.DeclaredConstant_$a2,$adef_Coq.ZArith.BinIntDef.Z.compare_$a2,$adef_Coq.setoid_ring.Ring_theory.ring_theory_$a8,$adef_PLF.Imp.AExp.aevalR_first_try.TooHardToRead.aevalR_$a2,$adef_Coq.QArith.QArith_base.Qden_$a1,$adef_PLF.Imp.BreakImp.CWhile_$a2,$adef_Coq.setoid_ring.InitialRing.gen_phiPOS_$a5,$adef_Coq.Init.Peano.IsSucc_$a1,$adef_Coq.NArith.BinNatDef.N.div2_$a1,$adef_Coq.Init.Datatypes.eq_true_$a1,$adef_$_case_Coq.Init.Datatypes.nat$111104_$a4,$adef_Coq.micromega.VarMap.Elt_$a2,$adef_PLF.Smallstep.Combined.test_$a3,$adef_Coq.Init.Decimal.Decimal_$a2,$adef_Coq.Init.Nat.tail_add_$a2,$adef_$_case_Coq.Init.Datatypes.nat$33979_$a5,$adef_Coq.Strings.Ascii.nat_of_ascii_$a1,$adef_Coq.micromega.ZMicromega.Vars.E.bits_lt_$a2,$adef_$_prop_141658_$a3,$adef_PLF.Smallstep.step_$a2,$adef_Coq.NArith.BinNat.N.peano_rect_$a1,$adef_Coq.Vectors.VectorDef.t_$a1,$adef_Coq.Bool.Bool.eqb_$a2,$adef_PLF.Imp.AExp.aevalR_$a2,$adef_Coq.micromega.RMicromega.CZ_$a1,$adef_Coq.ZArith.BinInt.Z.lt_$a2,$adef_Coq.setoid_ring.Field_theory.linear_$a1,$adef_Coq.Arith.PeanoNat.Nat.recursion_$a1,$adef_Coq.PArith.BinPosDef.Pos.eqb_$a2,$adef_Coq.Structures.OrderedTypeEx.String_as_OT.lts_$a2,$adef_Coq.ZArith.Zlogarithm.Is_power_$a1,$adef_Coq.Arith.PeanoNat.Nat.tail_add_$a2,$adef_Coq.ZArith.BinIntDef.Z.opp_$a1,$adef_Coq.Numbers.BinNums.Zneg_$a1,$adef_Coq.Reals.RIneq.mknonnegreal_$a1,$adef_Coq.Reals.Rdefinitions.Rgt_$a2,$adef_Coq.setoid_ring.Ring_polynom.PEpow_$a3,$adef_Coq.NArith.BinNatDef.N.to_nat_$a1,$adef_Coq.ZArith.Zeven.Zeven_$a1,$adef_Stlc.STLC.subst_$a3,$adef_Stlc.STLC.value_$a1,$adef_Coq.Bool.Bool.reflect_$a2,$adef_PLF.Imp.aevalR_division.AMult_$a2,$adef_Coq.setoid_ring.Ring_polynom.PX_$a4,$adef_Coq.Arith.Between.between_$a3,$adef_Coq.micromega.RingMicromega.PsatzIn_$a2,$adef_Coq.PArith.BinPosDef.Pos.sub_mask_$a2,$adef_PLF.Imp.AExp.ANum_$a1,$adef_Stlc.STLC.ty_rec_$a1,$adef_Coq.setoid_ring.Ring_polynom.PEI_$a1,$adef_Coq.Init.Specif.inright_$a2,$adef_$_fix_34955_v_CANONICAL_0_$a2,$adef_PLF.Imp.AExp.BEq_$a2,$adef_Stlc.STLC.substi_$a4,$adef_$_fix_34653_v_CANONICAL_0_$a2,$adef_Coq.setoid_ring.Ring_polynom.PEadd_$a3,$adef_Coq.setoid_ring.Field_theory.FEopp_$a2,$adef_Coq.Lists.SetoidList.eqlistA_$a4,$adef_Coq.Init.Specif.exist2_$a4,$adef_Coq.Init.Datatypes.CompareSpec_$a4,$adef_Coq.Init.Datatypes.xorb_$a2,$adef_Coq.Strings.String.String_$a2,$adef_PLF.Smallstep.Temp2.value_$a1,$adef_Coq.Relations.Relation_Definitions.equivalence_$a2,$adef_Coq.ZArith.Znumtheory.Euclid_intro_$a5,$adef_Coq.Init.Datatypes.CompEqT_$a3,$adef_Coq.micromega.RingMicromega.PsatzMulE_$a3,$adef_PLF.Smallstep.normal_form_of_$a2,$adef_Coq.Classes.Morphisms.respectful_$a4,$adef_Coq.micromega.Refl.make_impl_$a4,$adef_Coq.micromega.Tauto.FF_$a4,$adef_Coq.ZArith.BinIntDef.Z.abs_$a1,$adef_Coq.PArith.BinPosDef.Pos.min_$a2,$adef_Coq.FSets.FSetPositive.PositiveSet.In_$a2,$adef_Coq.Init.Nat.leb_$a2,$adef_Coq.NArith.BinNatDef.N.succ_$a1,$adef_Coq.Relations.Relation_Definitions.transitive_$a2,$adef_Coq.Structures.OrderedType.GT_$a5,$adef_PLF.Imp.AExp.aevalR_first_try.aevalR_$a2,$adef_Hammer.Tactics.Tactics.rdone_$a2,$adef_PLF.Imp.aevalR_division.ADiv_$a2,$adef_Coq.setoid_ring.Ring_theory.id_phi_N_$a1,$adef_Coq.Vectors.Fin.FS_$a2,$adef_$_case_Coq.Init.Datatypes.nat$150481_$a4,$adef_$_prop_141638_$a3,$adef_Coq.micromega.EnvRing.PExpr_$a1,$adef_$_prop_141640_$a3,$adef_PLF.Smallstep.aval_$a1,$adef_Coq.Setoids.Setoid.Setoid_Theory_$a2,$adef_Coq.Init.Peano.ge_$a2,$adef_Coq.Relations.Relation_Operators.clos_refl_trans_1n_$a4,$adef_Coq.Init.Decimal.Neg_$a1,$adef_$_case_Coq.Init.Datatypes.nat$34103_$a5,$adef_Coq.Lists.SetoidList.NoDupA_$a3,$adef_PLF.Imp.SLoad_$a1,$adef_PLF.Imp.aevalR_extended.AMult_$a2,$adef_Coq.Init.Decimal.D9_$a1,$adef_Coq.Logic.EqdepFacts.UIP_on__$a3,$adef_Coq.FSets.FSetPositive.PositiveSet.Subset_$a2,$adef_Coq.Init.Byte.byte_of_byte_$a1,$adef_Coq.Arith.EqNat.eq_nat_$a2,$adef_Coq.Init.Datatypes.nat_rect_$a4,$adef_$_case_Coq.Init.Datatypes.bool$166_$a4,$adef_Coq.micromega.Tauto.A_$a6,$adef_Coq.micromega.EnvRing.vmon_$a2,$adef_$_lam_32206_$a6,$adef_Coq.micromega.Tauto.X_$a5,$adef_Coq.setoid_ring.Field_theory.almost_field_theory_$a10,$adef_Coq.Arith.Wf_nat.ltof_$a4,$adef_Coq.Sorting.Sorted.Sorted_$a3,$adef_Coq.Init.Specif.sumor_$a2,$adef_Coq.micromega.RMicromega.CInv_$a1,$adef_Coq.PArith.BinPosDef.Pos.mul_$a2,$adef_Coq.PArith.BinPosDef.Pos.testbit_$a2,$adef_PLF.Smallstep.eval_$a2,$adef_Coq.ZArith.Znumtheory.rel_prime_$a2,$adef_Coq.NArith.BinNatDef.N.mul_$a2,$adef_Coq.Init.Nat.pred_$a1,$adef_Coq.Init.Specif.exist_$a3,$adef_PLF.Smallstep.stack_multistep_$a1,$adef_Coq.ZArith.BinInt.Z.le_$a2,$adef_Stlc.STLC.var_$a1,$adef_PLF.Imp.aevalR_extended.AMinus_$a2,$adef_PLF.Imp.CWhile_$a2,$adef_Coq.PArith.BinPosDef.Pos.compare_cont_$a1,$adef_$_case_Coq.Numbers.BinNums.positive$141708_$a2,$adef_PLF.Imp.BEq_$a2,$adef_Coq.Init.Specif.inleft_$a3,$adef_PLF.Imp.BreakImp.CSeq_$a2,$adef_Coq.micromega.EnvRing.Pinj_$a3,$adef_Coq.Init.Wf.well_founded_$a2,$adef_Coq.Init.Datatypes.cons_$a3,$adef_Coq.setoid_ring.Field_theory.field_theory_$a10,$adef_Coq.setoid_ring.Ring_theory.Computational_$a3,$adef_Coq.micromega.RingMicromega.PsatzSquare_$a2,$adef_Coq.Strings.String.string_dec_$a2,$adef_$_case_Coq.Init.Datatypes.nat$150695_$a4,$adef_Coq.ZArith.BinIntDef.Z.of_nat_$a1,$adef_Coq.Init.Datatypes.pair_$a4,$adef_Coq.Init.Decimal.int_of_int_$a1,$adef_Coq.PArith.BinPosDef.Pos.IsPos_$a1,$adef_$_prop_32_$a2,$adef_$_case_Coq.Init.Datatypes.nat$150789_$a4,$adef_Coq.PArith.BinPosDef.Pos.max_$a2,$adef_$_case_Coq.Init.Datatypes.bool$34518_$a5,$adef_Coq.ZArith.BinIntDef.Z.pow_pos_$a2,$adef_Coq.micromega.RingMicromega.Psatz_$a1,$adef_Coq.Init.Datatypes.Some_$a2,$adef_Coq.micromega.EnvRing.Pc_$a2,$adef_Coq.Structures.OrderedType.EQ_$a5,$adef_Coq.Numbers.BinNums.Zpos_$a1,$adef_PLF.Smallstep.normal_form_$a2,$adef_Coq.Init.Datatypes.list_$a1,$adef_Coq.Init.Nat.sub_$a2,$adef_$_case_Coq.Init.Datatypes.nat$150387_$a4,$adef_Coq.PArith.BinPos.Pos.SubMaskSpec_$a3,$adef_Coq.NArith.BinNatDef.N.add_$a2,$adef_PLF.Imp.AId_$a1,$adef_Coq.ZArith.BinInt.Z.divide_$a2,$adef_$_prop_141656_$a2,$adef_Coq.Bool.Bool.ReflectF_$a1,$adef_Coq.PArith.BinPos.Pos.iter_op_$a4,$adef_Coq.micromega.ZMicromega.Vars.Facts.MP.Dec.FSetDecideAuxiliary.FSet_Prop_$a1,$adef_Coq.Reals.Rfunctions.ZintNull_$a1,$adef_Coq.setoid_ring.Field_theory.FEI_$a1,$adef_Coq.micromega.EnvRing.PEX_$a2,$adef_Coq.Bool.Bool.ReflectT_$a1,$adef_Coq.ZArith.Znumtheory.Euclid_$a2,$adef_Stlc.STLC.substi_rect_$a3,$adef_Coq.Arith.PeanoNat.Nat.pred_$a1,$adef_Coq.Lists.List.Forall_$a3,$adef_$_case_Coq.Init.Datatypes.list$128598_$a6,$adef_$_case_Coq.Init.Datatypes.bool$34849_$a5,$adef_PLF.Smallstep.Combined.value_$a1,$adef_PLF.Smallstep.C_$a1,$adef_Coq.Init.Decimal.D5_$a1,$adef_Coq.PArith.BinPosDef.Pos.sub_$a2,$adef_Coq.NArith.BinNatDef.N.compare_$a2,$adef_Coq.Init.Decimal.uint_of_uint_$a1,$adef_Coq.Init.Datatypes.fst_$a3,$adef_PLF.Imp.aevalR_extended.aevalR_$a2,$adef_Coq.Arith.PeanoNat.Nat.sub_$a2,$adef_Coq.micromega.VarMap.Empty_$a1,$adef_Coq.micromega.RingMicromega.PsatzAdd_$a3,$adef_$_case_Coq.Init.Datatypes.nat$109110_$a4,$adef_Coq.PArith.BinPos.Pos.PeanoView_$a1,$adef_Coq.Init.Decimal.DecimalExp_$a3,$adef_Coq.ZArith.BinIntDef.Z.min_$a2,$adef_Coq.micromega.Tauto.N_$a5,$adef_PLF.Smallstep.Temp1.value_$a1,$adef_$_lam_142147_$a4,$adef_$_fix_33998_v_CANONICAL_0_$a2,$adef_PLF.Imp.CAss_$a2,$adef_PLF.Smallstep.relation_$a1,$adef_$_case_Coq.Init.Datatypes.nat$150586_$a4,$adef_Coq.Init.Nat.min_$a2,$adef_PLF.Imp.AExp.BLe_$a2,$adef_Coq.Init.Specif.existT2_$a6,$adef_Coq.micromega.RingMicromega.PsatzC_$a2,$adef_Stlc.STLC.Arrow_$a2,$adef_Coq.ZArith.BinInt.Zne_$a2,$adef_Coq.Reals.RIneq.Rsqr_$a1,$adef_Coq.PArith.BinPosDef.Pos.compare_$a2,$adef_$_prop_33_$a2,$adef_Coq.setoid_ring.InitialRing.mkhypo_$a2,$adef_Coq.Reals.RIneq.mknonzeroreal_$a1,$adef_Coq.ZArith.BinIntDef.Z.div_$a2,$adef_Coq.micromega.RingMicromega.PsatzZ_$a1,$adef_$_prop_141639_$a3,$adef_Coq.Bool.Bool.Is_true_$a1,$adef_Coq.Lists.List.fold_right_$a5,$adef_PLF.Imp.SPush_$a1,$adef_$_case_Coq.Init.Datatypes.nat$150278_$a4,$adef_$_let_var_6_p_139567_139570_$a4,$adef_Coq.NArith.BinNatDef.N.even_$a1,$adef_Coq.Arith.PeanoNat.Nat.max_$a2,$adef_Coq.setoid_ring.Field_theory.FEX_$a2,$adef_PLF.Imp.APlus_$a2,$adef_Coq.Lists.List.NoDup_$a2,$adef_Coq.Vectors.VectorDef.nil_$a1,$adef_PLF.Maps.total_map_$a1,$adef_Coq.ZArith.BinInt.Z.to_pos_$a1,$adef_PLF.Smallstep.Temp4.Temp5.step_$a2,$adef_Coq.Init.Specif.left_$a2,$adef_Coq.Init.Specif.sigT_$a2,$adef_$_case_Coq.Init.Datatypes.list$128685_$a3,$adef_Coq.Init.Decimal.D3_$a1,$adef_$_lam_149467_$a1,$adef_$_prop_141642_$a2,$adef_Coq.ZArith.BinIntDef.Z.pow_$a2,$adef_Coq.Relations.Relation_Operators.clos_refl_trans_n1_$a4,$adef_$_case_Coq.Init.Datatypes.nat$109001_$a4,$adef_PLF.Smallstep.CImp.CSeq_$a2,$adef_$_prop_141636_$a4,$adef_Coq.micromega.EnvRing.PX_$a4,$adef_Coq.micromega.EnvRing.PEadd_$a3,$adef_PLF.Imp.aevalR_division.aevalR_$a2,$adef_Coq.Vectors.Vector.Forall_$a4,$adef_Coq.Init.Specif.sig2_$a3,$adef_Coq.setoid_ring.Field_theory.FEpow_$a3,$adef_Coq.NArith.BinNat.N.eqf_$a2,$adef_Coq.micromega.ZMicromega.is_diff_env_elt_$a4,$adef_Coq.PArith.BinPos.Pos.div2_$a1,$adef_Coq.NArith.BinNat.N.le_$a2,$adef_Coq.Structures.DecidableTypeEx.Z_as_DT.lt_$a2,$adef_Coq.Vectors.Vector.cons_$a4,$adef_Coq.ZArith.Zpower.Zdiv_rest_proofs_$a2,$adef_Coq.PArith.BinPosDef.Pos.of_succ_nat_$a1,$adef_Coq.micromega.EnvRing.PEsub_$a3,$adef_PLF.Imp.aevalR_extended.ANum_$a1,$adef_Coq.PArith.BinPosDef.Pos.add_$a2,$adef_Coq.Init.Nat.double_$a1,$adef_Coq.Init.Peano.gt_$a2,$tdef_$_type_131740,$tdef_$_type_135084,$tdef_$_type_129016,$tdef_$_type_109499,$tdef_Coq.micromega.RingMicromega.Psatz,$tdef_Coq.ZArith.Znumtheory.Euclid,$tdef_$_type_31495,$tdef_$_type_148180,$tdef_Coq.micromega.ZMicromega.Vars.E.t,$tdef_Coq.Structures.OrderedTypeEx.Nat_as_OT.t,$tdef_$_type_142183,$tdef_$_type_141959,$tdef_$_type_141399,$tdef_$_type_149423,$tdef_$_type_127129,$tdef_$_type_113995,$tdef_$_type_121801,$tdef_Coq.ZArith.BinInt.Z.t,$tdef_Coq.micromega.EnvRing.Mon,$tdef_Coq.NArith.BinNat.N.t,$tdef_$_type_33788,$tdef_$_type_150500,$tdef_$_type_142103,$tdef_$_type_144097,$tdef_$_type_110533,$tdef_Coq.micromega.VarMap.t,$tdef_Coq.Reals.RIneq.nonposreal,$tdef_$_type_149579,$tdef_$_type_102913,$tdef_$_type_144443,$tdef_Coq.Init.Specif.sigT2,$tdef_$_type_124387,$tdef_$_type_124559,$tdef_$_type_30183,$tdef_$_type_30176,$tdef_$_type_140950,$tdef_$_type_31760,$tdef_$_type_141984,$tdef_$_type_126700,$tdef_$_type_35976,$tdef_$_type_102995,$tdef_$_type_149375,$tdef_Coq.Reals.RIneq.posreal,$tdef_$_type_142431,$tdef_$_type_113850,$tdef_Coq.Init.Datatypes.bool,$tdef_$_type_108568,$tdef_Coq.Init.Datatypes.list,$tdef_Coq.FSets.FSetPositive.PositiveSet.E.t,$tdef_Coq.Arith.PeanoNat.Nat.t,$tdef_$_type_108883,$tdef_$_type_102761,$tdef_$_type_139219,$tdef_$_type_143030,$tdef_$_type_142258,$tdef_$_type_129011,$tdef_$_type_134297,$tdef_Coq.Init.Decimal.decimal,$tdef_Coq.Structures.OrderedTypeEx.Positive_as_OT.t,$tdef_$_type_581,$tdef_$_type_124202,$tdef_PLF.Smallstep.relation,$tdef_$_type_142162,$tdef_Coq.Structures.OrdersTac.ord,$tdef_Coq.micromega.EnvRing.PExpr,$tdef_Coq.Init.Datatypes.option,$tdef_$_type_113838,$tdef_$_type_37,$tdef_$_type_139754,$tdef_$_type_127906,$tdef_Coq.PArith.BinPosDef.Pos.t,$tdef_$_type_109663,$tdef_$_type_101874,$tdef_$_type_36302,$tdef_$_type_110466,$tdef_$_type_140450,$tdef_$_type_127136,$tdef_$_type_107468,$tdef_$_type_172,$tdef_$_type_141341,$tdef_$_type_109738,$tdef_$_type_110399,$tdef_Coq.PArith.BinPos.Pos.mask,$tdef_$_type_141942,$tdef_Coq.Structures.OrderedTypeEx.PositiveOrderedTypeBits.t,$tdef_$_type_139282,$tdef_Coq.Structures.OrderedTypeEx.N_as_OT.t,$tdef_$_type_127761,$tdef_PLF.Smallstep.tm,$tdef_$_type_139982,$tdef_$_type_103090,$tdef_Coq.FSets.FSetPositive.PositiveSet.elt,$tdef_$_type_133213,$tdef_$_type_149007,$tdef_$_type_140023,$tdef_$_type_102795,$tdef_$_type_142131,$tdef_$_type_129019,$tdef_$_type_9,$tdef_$_type_111282,$tdef_$_type_138909,$tdef_$_type_143444,$tdef_$_type_101871,$tdef_PLF.Imp.state,$tdef_$_type_33424,$tdef_$_type_131953,$tdef_$_type_35971,$tdef_Coq.setoid_ring.Ring_polynom.Mon,$tdef_Coq.Init.Datatypes.comparison,$tdef_$_type_296,$tdef_$_type_142087,$tdef_$_type_134803,$tdef_$_type_143372,$tdef_$_type_132574,$tdef_$_type_124956,$tdef_$_type_109864,$tdef_PLF.Imp.BreakImp.com,$tdef_PLF.Imp.aexp,$tdef_$_type_113984,$tdef_Coq.micromega.Tauto.GFormula,$tdef_Coq.Numbers.BinNums.N,$tdef_PLF.Imp.BreakImp.result,$tdef_Coq.Init.Specif.sig2,$tdef_$_type_109711,$tdef_Coq.ZArith.BinIntDef.Z.t,$tdef_$_type_123086,$tdef_$_type_142079,$tdef_$_type_132166,$tdef_$_type_113836,$tdef_$_type_108886,$tdef_$_type_31804,$tdef_Coq.Init.Specif.sumbool,$tdef_PLF.Smallstep.Temp4.tm,$tdef_PLF.Smallstep.CImp.com,$tdef_$_type_121992,$tdef_$_type_142014,$tdef_$_type_101934,$tdef_$_type_121902,$tdef_$_type_148903,$tdef_$_type_148861,$tdef_$_type_130388,$tdef_$_type_109866,$tdef_Coq.Reals.Rdefinitions.R,$tdef_$_type_31247,$tdef_$_type_143051,$tdef_$_type_139002,$tdef_$_type_102799,$tdef_$_type_124863,$tdef_$_type_110563,$tdef_Coq.micromega.ZMicromega.ZWitness,$tdef_$_type_109731,$tdef_$_type_139959,$tdef_$_type_139530,$tdef_$_type_125038,$tdef_$_type_110395,$tdef_$_type_109671,$tdef_$_type_170,$tdef_$_type_107907,$tdef_$_type_103096,$tdef_$_type_141515,$tdef_$_type_141952,$tdef_PLF.Maps.total_map,$tdef_$_type_121700,$tdef_$_type_142466,$tdef_$_type_102809,$tdef_$_type_149404,$tdef_Coq.micromega.ZMicromega.ZArithProof,$tdef_$_type_128400,$tdef_$_type_30200,$tdef_$_type_142360,$tdef_Coq.Structures.DecidableTypeEx.Nat_as_DT.t,$tdef_$_type_323,$tdef_Coq.setoid_ring.Field_theory.FExpr,$tdef_Coq.Reals.RIneq.nonnegreal,$tdef_Coq.FSets.FSetPositive.PositiveSet.t,$tdef_$_type_32246,$tdef_$_type_138174,$tdef_Coq.micromega.RMicromega.Rcst,$tdef_$_type_113863,$tdef_$_type_31799,$tdef_$_type_109612,$tdef_Coq.Init.Datatypes.unit,$tdef_$_type_145804,$tdef_$_type_141979,$tdef_$_type_110635,$tdef_$_type_144789,$tdef_Coq.Init.Specif.sig,$tdef_$_type_113886,$tdef_Coq.Init.Datatypes.sum,$tdef_$_type_143033,$tdef_$_type_124138,$tdef_$_type_140575,$tdef_$_type_35968,$tdef_$_type_141061,$tdef_$_type_124770,$tdef_Coq.Strings.Ascii.ascii,$tdef_$_type_133816,$tdef_$_type_121245,$tdef_Coq.micromega.ZMicromega.Vars.elt,$tdef_Coq.FSets.FSetPositive.PositiveSet.tree,$tdef_$_type_141744,$tdef_$_type_130705,$tdef_$_type_133408,$tdef_Coq.Relations.Relation_Definitions.relation,$tdef_$_type_148858,$tdef_$_type_139581,$tdef_$_type_110521,$tdef_$_type_149237,$tdef_$_type_142151,$tdef_$_type_105,$tdef_$_type_102858,$tdef_$_type_131189,$tdef_Coq.Init.Nat.t,$tdef_Stlc.STLC.tm,$tdef_$_type_142180,$tdef_$_type_143562,$tdef_$_type_131243,$tdef_$_type_102878,$tdef_$_type_132787,$tdef_$_type_131327,$tdef_$_type_149186,$tdef_$_type_150184,$tdef_$_type_149080,$tdef_$_type_111446,$tdef_Coq.setoid_ring.Field_theory.linear,$tdef_$_type_35656,$tdef_$_type_133000,$tdef_$_type_109527,$tdef_PLF.Imp.com,$tdef_Coq.Init.Decimal.uint,$tdef_Prop,$tdef_$_type_130885,$tdef_$_type_33403,$tdef_$_type_133621,$tdef_Coq.Structures.DecidableTypeEx.Z_as_DT.t,$tdef_$_type_31685,$tdef_$_type_134389,$tdef_Coq.setoid_ring.InitialRing.hypo,$tdef_$_type_138466,$tdef_Coq.micromega.RingMicromega.Op2,$tdef_$_type_141966,$tdef_$_type_140825,$tdef_$_type_149366,$tdef_$_type_145458,$tdef_$_type_122349,$tdef_PLF.Imp.aevalR_division.aexp,$tdef_Coq.Init.Byte.byte,$tdef_$_type_138652,$tdef_Coq.Reals.Rfunctions.Z_spec,$tdef_Coq.Init.Decimal.int,$tdef_$_type_124353,$tdef_$_type_141886,$tdef_$_type_142090,$tdef_PLF.Imp.aevalR_extended.aexp,$tdef_PLF.Imp.AExp.bexp,$tdef_$_type_149541,$tdef_$_type_113888,$tdef_Coq.ZArith.Zpower.Zdiv_rest_proofs,$tdef_$_type_149042,$tdef_$_type_141907,$tdef_Coq.Strings.String.string,$tdef_$_type_36289,$tdef_$_type_30252,$tdef_$_type_102804,$tdef_$_type_145112,$tdef_$_type_143023,$tdef_$_type_36304,$tdef_$_type_128081,$tdef_$_type_108646,$tdef_$_type_139336,$tdef_Coq.Vectors.Vector.t,$tdef_PLF.Smallstep.prog,$tdef_$_type_123107,$tdef_$_type_111017,$tdef_$_type_114010,$tdef_$_type_146150,$tdef_Coq.Structures.DecidableTypeEx.Positive_as_DT.t,$tdef_$_type_36315,$tdef_$_type_35537,$tdef_$_type_31633,$tdef_$_type_102817,$tdef_$_type_139399,$tdef_Stlc.STLC.ty,$tdef_Coq.micromega.RingMicromega.Op1,$tdef_$_type_143511,$tdef_Coq.Init.Datatypes.CompareSpecT,$tdef_$_type_142108,$tdef_$_type_147165,$tdef_Coq.Init.Specif.sigT,$tdef_Coq.micromega.ZMicromega.coneMember,$tdef_$_type_143026,$tdef_$_type_127115,$tdef_PLF.Imp.sinstr,$tdef_$_type_109522,$tdef_$_type_122969,$tdef_$_type_142233,$tdef_$_type_147857,$tdef_$_type_33847,$tdef_$_type_142119,$tdef_$_type_110315,$tdef_$_type_138559,$tdef_$_type_30195,$tdef_$_type_132361,$tdef_Coq.setoid_ring.Field_theory.rsplit,$tdef_$_type_146842,$tdef_$_type_141300,$tdef_$_type_294,$tdef_$_type_111464,$tdef_Coq.micromega.EnvRing.Pol,$tdef_$_type_149484,$tdef_$_type_149258,$tdef_$_type_122295,$tdef_$_type_130822,$tdef_$_type_142384,$tdef_$_type_139832,$tdef_$_type_127754,$tdef_$_type_149108,$tdef_$_type_149479,$tdef_$_type_110478,$tdef_Coq.Structures.OrderedType.Compare,$tdef_Coq.Init.Specif.sumor,$tdef_$_type_137644,$tdef_$_type_122906,$tdef_$_type_134982,$tdef_$_type_140325,$tdef_$_type_149546,$tdef_Coq.Structures.DecidableTypeEx.N_as_DT.t,$tdef_$_type_99,$tdef_$_type_146496,$tdef_$_type_111344,$tdef_$_type_125213,$tdef_Coq.Structures.OrderedTypeEx.String_as_OT.t,$tdef_$_type_142222,$tdef_$_type_147511,$tdef_$_type_102973,$tdef_$_type_142093,$tdef_$_type_141351,$tdef_$_type_137546,$tdef_$_type_111461,$tdef_$_type_113852,$tdef_$_type_131159,$tdef_$_type_140049,$tdef_Coq.Bool.Bool.reflect,$tdef_Coq.PArith.BinPos.Pos.t,$tdef_$_type_32189,$tdef_$_type_148864,$tdef_$_type_102861,$tdef_$_type_102977,$tdef_Coq.setoid_ring.Ring_polynom.Pol,$tdef_$_type_122194,$tdef_$_type_33790,$tdef_$_type_108649,$tdef_$_type_134847,$tdef_$_type_102797,$tdef_$_type_131105,$tdef_$_type_142484,$tdef_$_type_141950,$tdef_$_type_33421,$tdef_$_type_128104,$tdef_$_type_130642,$tdef_$_type_134866,$tdef_$_type_122843,$tdef_Coq.Numbers.BinNums.Z,$tdef_Coq.QArith.QArith_base.Q,$tdef_$_type_134515,$tdef_$_type_140067,$tdef_$_type_109524,$tdef_Coq.PArith.BinPos.Pos.PeanoView,$tdef_Coq.Numbers.BinNums.positive,$tdef_$_type_35979,$tdef_Coq.Init.Datatypes.nat,$tdef_Coq.micromega.ZMicromega.Vars.t,$tdef_$_type_131219,$tdef_$_type_129008,$tdef_$_type_125131,$tdef_$_type_138270,$tdef_Coq.Structures.OrderedTypeEx.Z_as_OT.t,$tdef_$_type_123023,$tdef_$_type_139430,$tdef_Coq.Init.Datatypes.prod,$tdef_$_type_134247,$tdef_$_type_110639,$tdef_$_type_134767,$tdef_$_type_568,$tdef_Coq.micromega.RingMicromega.Formula,$tdef_$_type_299,$tdef_$_type_149243,$tdef_$_type_110366,$tdef_$_type_131135,$tdef_Coq.setoid_ring.Ring_polynom.PExpr,$tdef_Coq.micromega.RingMicromega.PolC,$tdef_$_type_31779,$tdef_$_type_381,$tdef_$_type_31978,$tdef_$_type_102,$tdef_$_type_134439,$tdef_$_type_122093,$tdef_$_type_141989,$tdef_$_type_101890,$tdef_PLF.Smallstep.Combined.tm,$tdef_Coq.NArith.BinNatDef.N.t,$tdef_Coq.Init.Datatypes.ID,$tdef_PLF.Imp.bexp,$tdef_Hammer.Tactics.Reconstr.ReconstrT,$tdef_$_type_110976,$tdef_$_type_149255,$tdef_$_type_143077,$tdef_$_type_141957,$tdef_$_type_149077,$tdef_$_type_148888,$tdef_$_type_143469,$tdef_$_type_125306,$tdef_$_type_576,$tdef_$_type_571,$tdef_$_type_113987,$tdef_Coq.setoid_ring.Ring_theory.ring_kind,$tdef_$_type_31263,$tdef_$_type_139793,$tdef_$_type_103030,$tdef_PLF.Smallstep.stack,$tdef_$_type_109506,$tdef_Coq.Vectors.VectorDef.t,$tdef_$_type_30197,$tdef_$_type_142306,$tdef_$_type_36328,$tdef_$_type_33416,$tdef_$_type_101888,$tdef_$_type_103022,$tdef_$_type_346,$tdef_$_type_141071,$tdef_$_type_131276,$tdef_$_type_102921,$tdef_$_type_140700,$tdef_$_type_148503,$tdef_Type,$tdef_Coq.PArith.BinPosDef.Pos.mask,$tdef_$_type_33429,$tdef_$_type_111392,$tdef_$_type_109503,$tdef_$_type_134723,$tdef_$_type_30212,$tdef_$_type_148849,$tdef_$_type_130768,$tdef_Coq.micromega.ZMicromega.Vars.tree,$tdef_Coq.Vectors.Fin.t,$tdef_$_type_143335,$tdef_$_type_143306,$tdef_Coq.Reals.RIneq.nonzeroreal,$tdef_$_type_109844,$tdef_$_type_35532,$tdef_$_type_140005,$tdef_$_type_33426,$tdef_$_type_142114,$tdef_$_type_114013,$tdef_PLF.Imp.AExp.aexp,$tdef_$_type_139156,$tdef_$_type_102905,$tdef_$_type_102854,$tdef_$_type_131300,$tdef_$_type_113891,$tdef_$_type_136804,$tdef_Coq.setoid_ring.InitialRing.Nword,$tdef_Coq.Reals.RIneq.negreal,$tdef_$_type_32678,$tdef_$_type_311,$tdef_$_type_103038,$tdef_$_type_138827,$tdef_$_type_149420,$tdef_$_type_114007,$tdef_$_type_30231,$tdef_$_type_142468,$tdef_$_type_139936,$tdef_$_type_134347,$tdef_$_type_148946,$tdef_$_type_149159,$tdef_$_type_138734]
% 15.80/15.87  ===============================================================
% 15.80/15.87  
% 15.80/15.87  Combined formula: 3118 axiom(s) => conjecture
% 15.80/15.87  
% 15.80/15.87  % Equality/functions detected -> nanoCoP oracle mode
% 15.80/15.87  nanoCoP : 
% 15.80/15.87  % 15,209,698 inferences, 12.758 CPU in 12.758 seconds (100% CPU, 1192183 Lips)
% 15.80/15.87  
% 15.80/15.87  % nanoCoP proof (equality/functions)
% 15.80/15.87  % nanoCoP proof is given at https://g4-mic.vidal-rosset.net/wasm/tinker via nanocop_proves(Your_Formula).
% 15.80/15.87  
% 15.80/15.87  % SZS output end Proof
%------------------------------------------------------------------------------