Dedup_before.sexp

 (VernacExpr()(VernacRequire()(false)(((v(Ident(Id List)))(loc(((fname(InFile Dedup_before.v))(line_nb 1)(bol_pos 0)(line_nb_last 1)(bol_pos_last 0)(bp 15)(ep 19))))))))
 (VernacExpr()(VernacImport false(((v(Ident(Id ListNotations)))(loc(((fname(InFile Dedup_before.v))(line_nb 2)(bol_pos 21)(line_nb_last 2)(bol_pos_last 21)(bp 28)(ep 41))))))))
 (VernacExpr()(VernacBeginSection((v(Id dedup))(loc(((fname(InFile Dedup_before.v))(line_nb 4)(bol_pos 44)(line_nb_last 4)(bol_pos_last 44)(bp 52)(ep 57)))))))
 (VernacExpr()(VernacAssumption(DoDischarge Definitional)NoInline((false(((((v(Id A))(loc(((fname(InFile Dedup_before.v))(line_nb 5)(bol_pos 59)(line_nb_last 5)(bol_pos_last 59)(bp 70)(ep 71)))))()))((v(CSort(GType())))(loc(((fname(InFile Dedup_before.v))(line_nb 5)(bol_pos 59)(line_nb_last 5)(bol_pos_last 59)(bp 74)(ep 78))))))))))
 (VernacExpr()(VernacAssumption(DoDischarge Logical)NoInline((false(((((v(Id A_eq_dec))(loc(((fname(InFile Dedup_before.v))(line_nb 6)(bol_pos 80)(line_nb_last 6)(bol_pos_last 80)(bp 93)(ep 101)))))()))((v(CProdN((CLocalAssum(((v(Name(Id x)))(loc(((fname(InFile Dedup_before.v))(line_nb 6)(bol_pos 80)(line_nb_last 6)(bol_pos_last 80)(bp 111)(ep 112)))))((v(Name(Id y)))(loc(((fname(InFile Dedup_before.v))(line_nb 6)(bol_pos 80)(line_nb_last 6)(bol_pos_last 80)(bp 113)(ep 114))))))(Default Explicit)((v(CRef((v(Ident(Id A)))(loc(((fname(InFile Dedup_before.v))(line_nb 6)(bol_pos 80)(line_nb_last 6)(bol_pos_last 80)(bp 117)(ep 118)))))()))(loc(((fname(InFile Dedup_before.v))(line_nb 6)(bol_pos 80)(line_nb_last 6)(bol_pos_last 80)(bp 117)(ep 118)))))))((v(CNotation"_ + _"((((v(CNotation"{ _ }"((((v(CNotation"_ = _"((((v(CRef((v(Ident(Id x)))(loc(((fname(InFile Dedup_before.v))(line_nb 6)(bol_pos 80)(line_nb_last 6)(bol_pos_last 80)(bp 121)(ep 122)))))()))(loc(((fname(InFile Dedup_before.v))(line_nb 6)(bol_pos 80)(line_nb_last 6)(bol_pos_last 80)(bp 121)(ep 122)))))((v(CRef((v(Ident(Id y)))(loc(((fname(InFile Dedup_before.v))(line_nb 6)(bol_pos 80)(line_nb_last 6)(bol_pos_last 80)(bp 125)(ep 126)))))()))(loc(((fname(InFile Dedup_before.v))(line_nb 6)(bol_pos 80)(line_nb_last 6)(bol_pos_last 80)(bp 125)(ep 126))))))()()())))(loc(((fname(InFile Dedup_before.v))(line_nb 6)(bol_pos 80)(line_nb_last 6)(bol_pos_last 80)(bp 121)(ep 126))))))()()())))(loc(((fname(InFile Dedup_before.v))(line_nb 6)(bol_pos 80)(line_nb_last 6)(bol_pos_last 80)(bp 120)(ep 127)))))((v(CNotation"{ _ }"((((v(CNotation"_ <> _"((((v(CRef((v(Ident(Id x)))(loc(((fname(InFile Dedup_before.v))(line_nb 6)(bol_pos 80)(line_nb_last 6)(bol_pos_last 80)(bp 131)(ep 132)))))()))(loc(((fname(InFile Dedup_before.v))(line_nb 6)(bol_pos 80)(line_nb_last 6)(bol_pos_last 80)(bp 131)(ep 132)))))((v(CRef((v(Ident(Id y)))(loc(((fname(InFile Dedup_before.v))(line_nb 6)(bol_pos 80)(line_nb_last 6)(bol_pos_last 80)(bp 136)(ep 137)))))()))(loc(((fname(InFile Dedup_before.v))(line_nb 6)(bol_pos 80)(line_nb_last 6)(bol_pos_last 80)(bp 136)(ep 137))))))()()())))(loc(((fname(InFile Dedup_before.v))(line_nb 6)(bol_pos 80)(line_nb_last 6)(bol_pos_last 80)(bp 131)(ep 137))))))()()())))(loc(((fname(InFile Dedup_before.v))(line_nb 6)(bol_pos 80)(line_nb_last 6)(bol_pos_last 80)(bp 130)(ep 138))))))()()())))(loc(((fname(InFile Dedup_before.v))(line_nb 6)(bol_pos 80)(line_nb_last 6)(bol_pos_last 80)(bp 120)(ep 138)))))))(loc(((fname(InFile Dedup_before.v))(line_nb 6)(bol_pos 80)(line_nb_last 6)(bol_pos_last 80)(bp 104)(ep 138))))))))))
 (VernacExpr()(VernacFixpoint NoDischarge((((((v(Id dedup))(loc(((fname(InFile Dedup_before.v))(line_nb 8)(bol_pos 141)(line_nb_last 8)(bol_pos_last 141)(bp 152)(ep 157)))))())(()CStructRec)((CLocalAssum(((v(Name(Id xs)))(loc(((fname(InFile Dedup_before.v))(line_nb 8)(bol_pos 141)(line_nb_last 8)(bol_pos_last 141)(bp 159)(ep 161))))))(Default Explicit)((v(CApp(()((v(CRef((v(Ident(Id list)))(loc(((fname(InFile Dedup_before.v))(line_nb 8)(bol_pos 141)(line_nb_last 8)(bol_pos_last 141)(bp 164)(ep 168)))))()))(loc(((fname(InFile Dedup_before.v))(line_nb 8)(bol_pos 141)(line_nb_last 8)(bol_pos_last 141)(bp 164)(ep 168))))))((((v(CRef((v(Ident(Id A)))(loc(((fname(InFile Dedup_before.v))(line_nb 8)(bol_pos 141)(line_nb_last 8)(bol_pos_last 141)(bp 169)(ep 170)))))()))(loc(((fname(InFile Dedup_before.v))(line_nb 8)(bol_pos 141)(line_nb_last 8)(bol_pos_last 141)(bp 169)(ep 170)))))()))))(loc(((fname(InFile Dedup_before.v))(line_nb 8)(bol_pos 141)(line_nb_last 8)(bol_pos_last 141)(bp 164)(ep 170)))))))((v(CApp(()((v(CRef((v(Ident(Id list)))(loc(((fname(InFile Dedup_before.v))(line_nb 8)(bol_pos 141)(line_nb_last 8)(bol_pos_last 141)(bp 174)(ep 178)))))()))(loc(((fname(InFile Dedup_before.v))(line_nb 8)(bol_pos 141)(line_nb_last 8)(bol_pos_last 141)(bp 174)(ep 178))))))((((v(CRef((v(Ident(Id A)))(loc(((fname(InFile Dedup_before.v))(line_nb 8)(bol_pos 141)(line_nb_last 8)(bol_pos_last 141)(bp 179)(ep 180)))))()))(loc(((fname(InFile Dedup_before.v))(line_nb 8)(bol_pos 141)(line_nb_last 8)(bol_pos_last 141)(bp 179)(ep 180)))))()))))(loc(((fname(InFile Dedup_before.v))(line_nb 8)(bol_pos 141)(line_nb_last 8)(bol_pos_last 141)(bp 174)(ep 180)))))(((v(CCases RegularStyle()((((v(CRef((v(Ident(Id xs)))(loc(((fname(InFile Dedup_before.v))(line_nb 9)(bol_pos 184)(line_nb_last 9)(bol_pos_last 184)(bp 194)(ep 196)))))()))(loc(((fname(InFile Dedup_before.v))(line_nb 9)(bol_pos 184)(line_nb_last 9)(bol_pos_last 184)(bp 194)(ep 196)))))()()))(((v(((((v(CPatNotation"[ ]"(()())()))(loc(((fname(InFile Dedup_before.v))(line_nb 10)(bol_pos 202)(line_nb_last 10)(bol_pos_last 202)(bp 208)(ep 210)))))))((v(CNotation"[ ]"(()()()())))(loc(((fname(InFile Dedup_before.v))(line_nb 10)(bol_pos 202)(line_nb_last 10)(bol_pos_last 202)(bp 214)(ep 216)))))))(loc(((fname(InFile Dedup_before.v))(line_nb 10)(bol_pos 202)(line_nb_last 10)(bol_pos_last 202)(bp 208)(ep 216)))))((v(((((v(CPatNotation"_ :: _"((((v(CPatAtom(((v(Ident(Id x)))(loc(((fname(InFile Dedup_before.v))(line_nb 11)(bol_pos 217)(line_nb_last 11)(bol_pos_last 217)(bp 223)(ep 224))))))))(loc(((fname(InFile Dedup_before.v))(line_nb 11)(bol_pos 217)(line_nb_last 11)(bol_pos_last 217)(bp 223)(ep 224)))))((v(CPatAtom(((v(Ident(Id xs)))(loc(((fname(InFile Dedup_before.v))(line_nb 11)(bol_pos 217)(line_nb_last 11)(bol_pos_last 217)(bp 228)(ep 230))))))))(loc(((fname(InFile Dedup_before.v))(line_nb 11)(bol_pos 217)(line_nb_last 11)(bol_pos_last 217)(bp 228)(ep 230))))))())()))(loc(((fname(InFile Dedup_before.v))(line_nb 11)(bol_pos 217)(line_nb_last 11)(bol_pos_last 217)(bp 223)(ep 230)))))))((v(CLetIn((v(Name(Id tail)))(loc(((fname(InFile Dedup_before.v))(line_nb 11)(bol_pos 217)(line_nb_last 11)(bol_pos_last 217)(bp 238)(ep 242)))))((v(CLambdaN()((v(CApp(()((v(CRef((v(Ident(Id dedup)))(loc(((fname(InFile Dedup_before.v))(line_nb 11)(bol_pos 217)(line_nb_last 11)(bol_pos_last 217)(bp 246)(ep 251)))))()))(loc(((fname(InFile Dedup_before.v))(line_nb 11)(bol_pos 217)(line_nb_last 11)(bol_pos_last 217)(bp 246)(ep 251))))))((((v(CRef((v(Ident(Id xs)))(loc(((fname(InFile Dedup_before.v))(line_nb 11)(bol_pos 217)(line_nb_last 11)(bol_pos_last 217)(bp 252)(ep 254)))))()))(loc(((fname(InFile Dedup_before.v))(line_nb 11)(bol_pos 217)(line_nb_last 11)(bol_pos_last 217)(bp 252)(ep 254)))))()))))(loc(((fname(InFile Dedup_before.v))(line_nb 11)(bol_pos 217)(line_nb_last 11)(bol_pos_last 217)(bp 246)(ep 254)))))))(loc(((fname(InFile Dedup_before.v))(line_nb 11)(bol_pos 217)(line_nb_last 11)(bol_pos_last 217)(bp 246)(ep 254)))))()((v(CIf((v(CApp(()((v(CRef((v(Ident(Id in_dec)))(loc(((fname(InFile Dedup_before.v))(line_nb 12)(bol_pos 258)(line_nb_last 12)(bol_pos_last 258)(bp 278)(ep 284)))))()))(loc(((fname(InFile Dedup_before.v))(line_nb 12)(bol_pos 258)(line_nb_last 12)(bol_pos_last 258)(bp 278)(ep 284))))))((((v(CRef((v(Ident(Id A_eq_dec)))(loc(((fname(InFile Dedup_before.v))(line_nb 12)(bol_pos 258)(line_nb_last 12)(bol_pos_last 258)(bp 285)(ep 293)))))()))(loc(((fname(InFile Dedup_before.v))(line_nb 12)(bol_pos 258)(line_nb_last 12)(bol_pos_last 258)(bp 285)(ep 293)))))())(((v(CRef((v(Ident(Id x)))(loc(((fname(InFile Dedup_before.v))(line_nb 12)(bol_pos 258)(line_nb_last 12)(bol_pos_last 258)(bp 294)(ep 295)))))()))(loc(((fname(InFile Dedup_before.v))(line_nb 12)(bol_pos 258)(line_nb_last 12)(bol_pos_last 258)(bp 294)(ep 295)))))())(((v(CRef((v(Ident(Id xs)))(loc(((fname(InFile Dedup_before.v))(line_nb 12)(bol_pos 258)(line_nb_last 12)(bol_pos_last 258)(bp 296)(ep 298)))))()))(loc(((fname(InFile Dedup_before.v))(line_nb 12)(bol_pos 258)(line_nb_last 12)(bol_pos_last 258)(bp 296)(ep 298)))))()))))(loc(((fname(InFile Dedup_before.v))(line_nb 12)(bol_pos 258)(line_nb_last 12)(bol_pos_last 258)(bp 278)(ep 298)))))(()())((v(CRef((v(Ident(Id tail)))(loc(((fname(InFile Dedup_before.v))(line_nb 13)(bol_pos 304)(line_nb_last 13)(bol_pos_last 304)(bp 323)(ep 327)))))()))(loc(((fname(InFile Dedup_before.v))(line_nb 13)(bol_pos 304)(line_nb_last 13)(bol_pos_last 304)(bp 323)(ep 327)))))((v(CNotation"_ :: _"((((v(CRef((v(Ident(Id x)))(loc(((fname(InFile Dedup_before.v))(line_nb 15)(bol_pos 350)(line_nb_last 15)(bol_pos_last 350)(bp 369)(ep 370)))))()))(loc(((fname(InFile Dedup_before.v))(line_nb 15)(bol_pos 350)(line_nb_last 15)(bol_pos_last 350)(bp 369)(ep 370)))))((v(CRef((v(Ident(Id tail)))(loc(((fname(InFile Dedup_before.v))(line_nb 15)(bol_pos 350)(line_nb_last 15)(bol_pos_last 350)(bp 374)(ep 378)))))()))(loc(((fname(InFile Dedup_before.v))(line_nb 15)(bol_pos 350)(line_nb_last 15)(bol_pos_last 350)(bp 374)(ep 378))))))()()())))(loc(((fname(InFile Dedup_before.v))(line_nb 15)(bol_pos 350)(line_nb_last 15)(bol_pos_last 350)(bp 369)(ep 378)))))))(loc(((fname(InFile Dedup_before.v))(line_nb 12)(bol_pos 258)(line_nb_last 15)(bol_pos_last 350)(bp 275)(ep 378)))))))(loc(((fname(InFile Dedup_before.v))(line_nb 11)(bol_pos 217)(line_nb_last 15)(bol_pos_last 350)(bp 234)(ep 378)))))))(loc(((fname(InFile Dedup_before.v))(line_nb 11)(bol_pos 217)(line_nb_last 15)(bol_pos_last 350)(bp 223)(ep 378))))))))(loc(((fname(InFile Dedup_before.v))(line_nb 9)(bol_pos 184)(line_nb_last 16)(bol_pos_last 379)(bp 188)(ep 386)))))))()))))
 (VernacExpr()(VernacStartTheoremProof Lemma(((((v(Id dedup_In))(loc(((fname(InFile Dedup_before.v))(line_nb 18)(bol_pos 389)(line_nb_last 18)(bol_pos_last 389)(bp 397)(ep 405)))))())(()((v(CProdN((CLocalAssum(((v(Name(Id x)))(loc(((fname(InFile Dedup_before.v))(line_nb 18)(bol_pos 389)(line_nb_last 18)(bol_pos_last 389)(bp 416)(ep 417))))))(Default Explicit)((v(CRef((v(Ident(Id A)))(loc(((fname(InFile Dedup_before.v))(line_nb 18)(bol_pos 389)(line_nb_last 18)(bol_pos_last 389)(bp 420)(ep 421)))))()))(loc(((fname(InFile Dedup_before.v))(line_nb 18)(bol_pos 389)(line_nb_last 18)(bol_pos_last 389)(bp 420)(ep 421))))))(CLocalAssum(((v(Name(Id xs)))(loc(((fname(InFile Dedup_before.v))(line_nb 18)(bol_pos 389)(line_nb_last 18)(bol_pos_last 389)(bp 423)(ep 425))))))(Default Explicit)((v(CHole()IntroAnonymous()))(loc(((fname(InFile Dedup_before.v))(line_nb 18)(bol_pos 389)(line_nb_last 18)(bol_pos_last 389)(bp 423)(ep 425)))))))((v(CNotation"_ -> _"((((v(CApp(()((v(CRef((v(Ident(Id In)))(loc(((fname(InFile Dedup_before.v))(line_nb 19)(bol_pos 427)(line_nb_last 19)(bol_pos_last 427)(bp 433)(ep 435)))))()))(loc(((fname(InFile Dedup_before.v))(line_nb 19)(bol_pos 427)(line_nb_last 19)(bol_pos_last 427)(bp 433)(ep 435))))))((((v(CRef((v(Ident(Id x)))(loc(((fname(InFile Dedup_before.v))(line_nb 19)(bol_pos 427)(line_nb_last 19)(bol_pos_last 427)(bp 436)(ep 437)))))()))(loc(((fname(InFile Dedup_before.v))(line_nb 19)(bol_pos 427)(line_nb_last 19)(bol_pos_last 427)(bp 436)(ep 437)))))())(((v(CRef((v(Ident(Id xs)))(loc(((fname(InFile Dedup_before.v))(line_nb 19)(bol_pos 427)(line_nb_last 19)(bol_pos_last 427)(bp 438)(ep 440)))))()))(loc(((fname(InFile Dedup_before.v))(line_nb 19)(bol_pos 427)(line_nb_last 19)(bol_pos_last 427)(bp 438)(ep 440)))))()))))(loc(((fname(InFile Dedup_before.v))(line_nb 19)(bol_pos 427)(line_nb_last 19)(bol_pos_last 427)(bp 433)(ep 440)))))((v(CApp(()((v(CRef((v(Ident(Id In)))(loc(((fname(InFile Dedup_before.v))(line_nb 20)(bol_pos 444)(line_nb_last 20)(bol_pos_last 444)(bp 450)(ep 452)))))()))(loc(((fname(InFile Dedup_before.v))(line_nb 20)(bol_pos 444)(line_nb_last 20)(bol_pos_last 444)(bp 450)(ep 452))))))((((v(CRef((v(Ident(Id x)))(loc(((fname(InFile Dedup_before.v))(line_nb 20)(bol_pos 444)(line_nb_last 20)(bol_pos_last 444)(bp 453)(ep 454)))))()))(loc(((fname(InFile Dedup_before.v))(line_nb 20)(bol_pos 444)(line_nb_last 20)(bol_pos_last 444)(bp 453)(ep 454)))))())(((v(CApp(()((v(CRef((v(Ident(Id dedup)))(loc(((fname(InFile Dedup_before.v))(line_nb 20)(bol_pos 444)(line_nb_last 20)(bol_pos_last 444)(bp 456)(ep 461)))))()))(loc(((fname(InFile Dedup_before.v))(line_nb 20)(bol_pos 444)(line_nb_last 20)(bol_pos_last 444)(bp 456)(ep 461))))))((((v(CRef((v(Ident(Id xs)))(loc(((fname(InFile Dedup_before.v))(line_nb 20)(bol_pos 444)(line_nb_last 20)(bol_pos_last 444)(bp 462)(ep 464)))))()))(loc(((fname(InFile Dedup_before.v))(line_nb 20)(bol_pos 444)(line_nb_last 20)(bol_pos_last 444)(bp 462)(ep 464)))))()))))(loc(((fname(InFile Dedup_before.v))(line_nb 20)(bol_pos 444)(line_nb_last 20)(bol_pos_last 444)(bp 456)(ep 464)))))()))))(loc(((fname(InFile Dedup_before.v))(line_nb 20)(bol_pos 444)(line_nb_last 20)(bol_pos_last 444)(bp 450)(ep 465))))))()()())))(loc(((fname(InFile Dedup_before.v))(line_nb 19)(bol_pos 427)(line_nb_last 20)(bol_pos_last 444)(bp 433)(ep 465)))))))(loc(((fname(InFile Dedup_before.v))(line_nb 18)(bol_pos 389)(line_nb_last 20)(bol_pos_last 444)(bp 408)(ep 465))))))))))
 (VernacExpr()(VernacProof()(SsEmpty)))
 (VernacExpr()(VernacExtend(VernacSolve 0)((GenArg raw(OptArg(ExtraArg ltac_selector))())(GenArg raw(OptArg(ExtraArg ltac_info))())(GenArg raw(ExtraArg tactic)(TacThen(TacThen(TacAtom((((fname(InFile Dedup_before.v))(line_nb 22)(bol_pos 482)(line_nb_last 22)(bol_pos_last 482)(bp 486)(ep 498)))(TacInductionDestruct true false((((()(ElimOnIdent((v(Id xs))(loc(((fname(InFile Dedup_before.v))(line_nb 22)(bol_pos 482)(line_nb_last 22)(bol_pos_last 482)(bp 496)(ep 498)))))))(()())()))()))))(TacAtom((((fname(InFile Dedup_before.v))(line_nb 22)(bol_pos 482)(line_nb_last 22)(bol_pos_last 482)(bp 500)(ep 506)))(TacIntroPattern false(((v(IntroForthcoming false))(loc(((fname(InFile Dedup_before.v))(line_nb 22)(bol_pos 482)(line_nb_last 22)(bol_pos_last 482)(bp 500)(ep 506))))))))))(TacAtom((((fname(InFile Dedup_before.v))(line_nb 22)(bol_pos 482)(line_nb_last 22)(bol_pos_last 482)(bp 508)(ep 518)))(TacReduce(Simpl((rBeta true)(rMatch true)(rFix true)(rCofix true)(rZeta true)(rDelta true)(rConst()))())((onhyps())(concl_occs AllOccurrences)))))))(GenArg raw(ExtraArg ltac_use_default)false))))
 (VernacExpr()(VernacBullet(Dash 1)))
 (VernacExpr()(VernacExtend(VernacSolve 0)((GenArg raw(OptArg(ExtraArg ltac_selector))())(GenArg raw(OptArg(ExtraArg ltac_info))())(GenArg raw(ExtraArg tactic)(TacAlias((((fname(InFile Dedup_before.v))(line_nb 23)(bol_pos 520)(line_nb_last 23)(bol_pos_last 520)(bp 526)(ep 535)))((Kername(MPfile(DirPath((Id Tauto)(Id Init)(Id Coq))))(DirPath())(Id intuition_3AD8AF16))()))))(GenArg raw(ExtraArg ltac_use_default)false))))
 (VernacExpr()(VernacBullet(Dash 1)))
 (VernacExpr()(VernacExtend(VernacSolve 0)((GenArg raw(OptArg(ExtraArg ltac_selector))())(GenArg raw(OptArg(ExtraArg ltac_info))())(GenArg raw(ExtraArg tactic)(TacThen(TacThen(TacThen(TacThen(TacAtom((((fname(InFile Dedup_before.v))(line_nb 24)(bol_pos 537)(line_nb_last 24)(bol_pos_last 537)(bp 543)(ep 554)))(TacCase false(()(((v(CRef((v(Ident(Id in_dec)))(loc(((fname(InFile Dedup_before.v))(line_nb 24)(bol_pos 537)(line_nb_last 24)(bol_pos_last 537)(bp 548)(ep 554)))))()))(loc()))NoBindings)))))(TacAlias((((fname(InFile Dedup_before.v))(line_nb 24)(bol_pos 537)(line_nb_last 24)(bol_pos_last 537)(bp 556)(ep 565)))((Kername(MPfile(DirPath((Id Tauto)(Id Init)(Id Coq))))(DirPath())(Id intuition_3AD8AF16))()))))(TacAlias((((fname(InFile Dedup_before.v))(line_nb 24)(bol_pos 537)(line_nb_last 24)(bol_pos_last 537)(bp 567)(ep 572)))((Kername(MPfile(DirPath((Id Notations)(Id Init)(Id Coq))))(DirPath())(Id subst_4C69D532))()))))(TacAtom((((fname(InFile Dedup_before.v))(line_nb 24)(bol_pos 537)(line_nb_last 24)(bol_pos_last 537)(bp 574)(ep 579)))(TacReduce(Simpl((rBeta true)(rMatch true)(rFix true)(rCofix true)(rZeta true)(rDelta true)(rConst()))())((onhyps(()))(concl_occs AllOccurrences))))))(TacAlias((((fname(InFile Dedup_before.v))(line_nb 24)(bol_pos 537)(line_nb_last 24)(bol_pos_last 537)(bp 581)(ep 585)))((Kername(MPfile(DirPath((Id Notations)(Id Init)(Id Coq))))(DirPath())(Id auto_#_#_#_4C69D5ED))((TacGeneric(GenArg raw(OptArg(ExtraArg int_or_var))()))(TacGeneric(GenArg raw(ExtraArg auto_using)()))(TacGeneric(GenArg raw(ExtraArg hintbases)(())))))))))(GenArg raw(ExtraArg ltac_use_default)false))))
 (VernacExpr()(VernacEndProof(Proved Opaque())))
 (VernacExpr()(VernacEndSegment((v(Id dedup))(loc(((fname(InFile Dedup_before.v))(line_nb 26)(bol_pos 594)(line_nb_last 26)(bol_pos_last 594)(bp 598)(ep 603)))))))