{"meta":{"exporter":{"name":"lean4export","version":"3.1.0"},"format":{"version":"3.1.0"},"lean":{"githash":"11acb17ec6b07a8f9e9173e6845197929540936b","version":"4.35.0-rc2"}}}
{"in":1,"str":{"pre":0,"str":"Nat"}}
{"il":1,"succ":0}
{"ie":0,"sort":1}
{"in":2,"str":{"pre":1,"str":"zero"}}
{"in":3,"str":{"pre":1,"str":"succ"}}
{"const":{"name":1,"us":[]},"ie":1}
{"in":4,"str":{"pre":0,"str":"n"}}
{"forallE":{"binderInfo":"default","body":1,"name":4,"type":1},"ie":2}
{"in":5,"str":{"pre":1,"str":"rec"}}
{"in":6,"str":{"pre":0,"str":"u"}}
{"il":2,"param":6}
{"in":7,"str":{"pre":0,"str":"motive"}}
{"in":8,"str":{"pre":0,"str":"t"}}
{"ie":3,"sort":2}
{"forallE":{"binderInfo":"default","body":3,"name":8,"type":1},"ie":4}
{"in":9,"str":{"pre":0,"str":"zero"}}
{"bvar":0,"ie":5}
{"const":{"name":2,"us":[]},"ie":6}
{"app":{"arg":6,"fn":5},"ie":7}
{"in":10,"str":{"pre":0,"str":"succ"}}
{"in":11,"str":{"pre":0,"str":"n_ih"}}
{"bvar":2,"ie":8}
{"app":{"arg":5,"fn":8},"ie":9}
{"bvar":3,"ie":10}
{"const":{"name":3,"us":[]},"ie":11}
{"bvar":1,"ie":12}
{"app":{"arg":12,"fn":11},"ie":13}
{"app":{"arg":13,"fn":10},"ie":14}
{"forallE":{"binderInfo":"default","body":14,"name":11,"type":9},"ie":15}
{"forallE":{"binderInfo":"default","body":15,"name":4,"type":1},"ie":16}
{"app":{"arg":5,"fn":10},"ie":17}
{"forallE":{"binderInfo":"default","body":17,"name":8,"type":1},"ie":18}
{"forallE":{"binderInfo":"default","body":18,"name":10,"type":16},"ie":19}
{"forallE":{"binderInfo":"default","body":19,"name":9,"type":7},"ie":20}
{"forallE":{"binderInfo":"implicit","body":20,"name":7,"type":4},"ie":21}
{"ie":22,"lam":{"binderInfo":"default","body":12,"name":10,"type":16}}
{"ie":23,"lam":{"binderInfo":"default","body":22,"name":9,"type":7}}
{"ie":24,"lam":{"binderInfo":"default","body":23,"name":7,"type":4}}
{"app":{"arg":5,"fn":12},"ie":25}
{"const":{"name":5,"us":[2]},"ie":26}
{"app":{"arg":10,"fn":26},"ie":27}
{"app":{"arg":8,"fn":27},"ie":28}
{"app":{"arg":12,"fn":28},"ie":29}
{"app":{"arg":5,"fn":29},"ie":30}
{"app":{"arg":30,"fn":25},"ie":31}
{"ie":32,"lam":{"binderInfo":"default","body":31,"name":4,"type":1}}
{"ie":33,"lam":{"binderInfo":"default","body":32,"name":10,"type":16}}
{"ie":34,"lam":{"binderInfo":"default","body":33,"name":9,"type":7}}
{"ie":35,"lam":{"binderInfo":"default","body":34,"name":7,"type":4}}
{"inductive":{"ctors":[{"cidx":0,"induct":1,"isUnsafe":false,"levelParams":[],"name":2,"numFields":0,"numParams":0,"type":1},{"cidx":1,"induct":1,"isUnsafe":false,"levelParams":[],"name":3,"numFields":1,"numParams":0,"type":2}],"recs":[{"all":[1],"isUnsafe":false,"k":false,"levelParams":[6],"name":5,"numIndices":0,"numMinors":2,"numMotives":1,"numParams":0,"rules":[{"ctor":2,"nfields":0,"rhs":24},{"ctor":3,"nfields":1,"rhs":35}],"type":21}],"types":[{"all":[1],"ctors":[2,3],"isRec":true,"isReflexive":false,"isUnsafe":false,"levelParams":[],"name":1,"numIndices":0,"numNested":0,"numParams":0,"type":0}]}}
{"in":12,"str":{"pre":0,"str":"Eq"}}
{"in":13,"str":{"pre":0,"str":"u_1"}}
{"il":3,"param":13}
{"in":14,"str":{"pre":0,"str":"α"}}
{"ie":36,"sort":3}
{"in":15,"str":{"pre":0,"str":"a"}}
{"in":16,"str":{"pre":15,"str":"_@"}}
{"in":17,"str":{"pre":16,"str":"_internal"}}
{"in":18,"str":{"pre":17,"str":"_hyg"}}
{"in":19,"num":{"i":0,"pre":18}}
{"ie":37,"sort":0}
{"forallE":{"binderInfo":"default","body":37,"name":19,"type":12},"ie":38}
{"forallE":{"binderInfo":"default","body":38,"name":19,"type":5},"ie":39}
{"forallE":{"binderInfo":"implicit","body":39,"name":14,"type":36},"ie":40}
{"in":20,"str":{"pre":12,"str":"refl"}}
{"const":{"name":12,"us":[3]},"ie":41}
{"app":{"arg":12,"fn":41},"ie":42}
{"app":{"arg":5,"fn":42},"ie":43}
{"app":{"arg":5,"fn":43},"ie":44}
{"forallE":{"binderInfo":"default","body":44,"name":15,"type":5},"ie":45}
{"forallE":{"binderInfo":"implicit","body":45,"name":14,"type":36},"ie":46}
{"in":21,"str":{"pre":12,"str":"rec"}}
{"app":{"arg":8,"fn":41},"ie":47}
{"app":{"arg":12,"fn":47},"ie":48}
{"app":{"arg":5,"fn":48},"ie":49}
{"forallE":{"binderInfo":"default","body":3,"name":8,"type":49},"ie":50}
{"forallE":{"binderInfo":"default","body":50,"name":19,"type":12},"ie":51}
{"in":22,"str":{"pre":0,"str":"refl"}}
{"app":{"arg":12,"fn":5},"ie":52}
{"const":{"name":20,"us":[3]},"ie":53}
{"app":{"arg":8,"fn":53},"ie":54}
{"app":{"arg":12,"fn":54},"ie":55}
{"app":{"arg":55,"fn":52},"ie":56}
{"bvar":4,"ie":57}
{"app":{"arg":57,"fn":41},"ie":58}
{"app":{"arg":10,"fn":58},"ie":59}
{"app":{"arg":5,"fn":59},"ie":60}
{"app":{"arg":12,"fn":10},"ie":61}
{"app":{"arg":5,"fn":61},"ie":62}
{"forallE":{"binderInfo":"default","body":62,"name":8,"type":60},"ie":63}
{"forallE":{"binderInfo":"implicit","body":63,"name":19,"type":10},"ie":64}
{"forallE":{"binderInfo":"default","body":64,"name":22,"type":56},"ie":65}
{"forallE":{"binderInfo":"implicit","body":65,"name":7,"type":51},"ie":66}
{"forallE":{"binderInfo":"implicit","body":66,"name":19,"type":5},"ie":67}
{"forallE":{"binderInfo":"implicit","body":67,"name":14,"type":36},"ie":68}
{"ie":69,"lam":{"binderInfo":"default","body":5,"name":22,"type":56}}
{"ie":70,"lam":{"binderInfo":"default","body":69,"name":7,"type":51}}
{"ie":71,"lam":{"binderInfo":"default","body":70,"name":19,"type":5}}
{"ie":72,"lam":{"binderInfo":"implicit","body":71,"name":14,"type":36}}
{"inductive":{"ctors":[{"cidx":0,"induct":12,"isUnsafe":false,"levelParams":[13],"name":20,"numFields":0,"numParams":2,"type":46}],"recs":[{"all":[12],"isUnsafe":false,"k":true,"levelParams":[6,13],"name":21,"numIndices":1,"numMinors":1,"numMotives":1,"numParams":2,"rules":[{"ctor":20,"nfields":0,"rhs":72}],"type":68}],"types":[{"all":[12],"ctors":[20],"isRec":false,"isReflexive":false,"isUnsafe":false,"levelParams":[13],"name":12,"numIndices":1,"numNested":0,"numParams":2,"type":40}]}}
{"in":23,"str":{"pre":0,"str":"outParam"}}
{"forallE":{"binderInfo":"default","body":3,"name":14,"type":3},"ie":73}
{"ie":74,"lam":{"binderInfo":"default","body":5,"name":14,"type":3}}
{"def":{"all":[23],"hints":{"regular":1},"levelParams":[6],"name":23,"safety":"safe","type":73,"value":74}}
{"in":24,"str":{"pre":0,"str":"HAdd"}}
{"in":25,"str":{"pre":0,"str":"v"}}
{"in":26,"str":{"pre":0,"str":"w"}}
{"il":4,"param":25}
{"il":5,"param":26}
{"il":6,"succ":2}
{"ie":75,"sort":6}
{"in":27,"str":{"pre":0,"str":"β"}}
{"il":7,"succ":4}
{"ie":76,"sort":7}
{"in":28,"str":{"pre":0,"str":"γ"}}
{"il":8,"succ":5}
{"il":9,"succ":8}
{"const":{"name":23,"us":[9]},"ie":77}
{"ie":78,"sort":8}
{"app":{"arg":78,"fn":77},"ie":79}
{"il":10,"max":[6,7]}
{"il":11,"max":[10,8]}
{"ie":80,"sort":11}
{"forallE":{"binderInfo":"default","body":80,"name":28,"type":79},"ie":81}
{"forallE":{"binderInfo":"default","body":81,"name":27,"type":76},"ie":82}
{"forallE":{"binderInfo":"default","body":82,"name":14,"type":75},"ie":83}
{"in":29,"str":{"pre":24,"str":"mk"}}
{"in":30,"str":{"pre":0,"str":"hAdd"}}
{"forallE":{"binderInfo":"default","body":8,"name":19,"type":8},"ie":84}
{"forallE":{"binderInfo":"default","body":84,"name":19,"type":8},"ie":85}
{"const":{"name":24,"us":[2,4,5]},"ie":86}
{"app":{"arg":10,"fn":86},"ie":87}
{"app":{"arg":8,"fn":87},"ie":88}
{"app":{"arg":12,"fn":88},"ie":89}
{"forallE":{"binderInfo":"default","body":89,"name":30,"type":85},"ie":90}
{"forallE":{"binderInfo":"implicit","body":90,"name":28,"type":79},"ie":91}
{"forallE":{"binderInfo":"implicit","body":91,"name":27,"type":76},"ie":92}
{"forallE":{"binderInfo":"implicit","body":92,"name":14,"type":75},"ie":93}
{"in":31,"str":{"pre":24,"str":"rec"}}
{"app":{"arg":8,"fn":86},"ie":94}
{"app":{"arg":12,"fn":94},"ie":95}
{"app":{"arg":5,"fn":95},"ie":96}
{"forallE":{"binderInfo":"default","body":36,"name":8,"type":96},"ie":97}
{"in":32,"str":{"pre":0,"str":"mk"}}
{"forallE":{"binderInfo":"default","body":10,"name":19,"type":10},"ie":98}
{"forallE":{"binderInfo":"default","body":98,"name":19,"type":10},"ie":99}
{"const":{"name":29,"us":[2,4,5]},"ie":100}
{"app":{"arg":57,"fn":100},"ie":101}
{"app":{"arg":10,"fn":101},"ie":102}
{"app":{"arg":8,"fn":102},"ie":103}
{"app":{"arg":5,"fn":103},"ie":104}
{"app":{"arg":104,"fn":12},"ie":105}
{"forallE":{"binderInfo":"default","body":105,"name":30,"type":99},"ie":106}
{"app":{"arg":57,"fn":86},"ie":107}
{"app":{"arg":10,"fn":107},"ie":108}
{"app":{"arg":8,"fn":108},"ie":109}
{"forallE":{"binderInfo":"default","body":9,"name":8,"type":109},"ie":110}
{"forallE":{"binderInfo":"default","body":110,"name":32,"type":106},"ie":111}
{"forallE":{"binderInfo":"implicit","body":111,"name":7,"type":97},"ie":112}
{"forallE":{"binderInfo":"implicit","body":112,"name":28,"type":78},"ie":113}
{"forallE":{"binderInfo":"implicit","body":113,"name":27,"type":76},"ie":114}
{"forallE":{"binderInfo":"implicit","body":114,"name":14,"type":75},"ie":115}
{"forallE":{"binderInfo":"default","body":57,"name":19,"type":57},"ie":116}
{"forallE":{"binderInfo":"default","body":116,"name":19,"type":57},"ie":117}
{"ie":118,"lam":{"binderInfo":"default","body":25,"name":30,"type":117}}
{"ie":119,"lam":{"binderInfo":"default","body":118,"name":32,"type":106}}
{"ie":120,"lam":{"binderInfo":"default","body":119,"name":7,"type":97}}
{"ie":121,"lam":{"binderInfo":"default","body":120,"name":28,"type":78}}
{"ie":122,"lam":{"binderInfo":"default","body":121,"name":27,"type":76}}
{"ie":123,"lam":{"binderInfo":"default","body":122,"name":14,"type":75}}
{"inductive":{"ctors":[{"cidx":0,"induct":24,"isUnsafe":false,"levelParams":[6,25,26],"name":29,"numFields":1,"numParams":3,"type":93}],"recs":[{"all":[24],"isUnsafe":false,"k":false,"levelParams":[13,6,25,26],"name":31,"numIndices":0,"numMinors":1,"numMotives":1,"numParams":3,"rules":[{"ctor":29,"nfields":1,"rhs":123}],"type":115}],"types":[{"all":[24],"ctors":[29],"isRec":false,"isReflexive":false,"isUnsafe":false,"levelParams":[6,25,26],"name":24,"numIndices":0,"numNested":0,"numParams":3,"type":83}]}}
{"in":33,"str":{"pre":24,"str":"hAdd"}}
{"in":34,"str":{"pre":0,"str":"self"}}
{"forallE":{"binderInfo":"instImplicit","body":99,"name":34,"type":96},"ie":124}
{"forallE":{"binderInfo":"implicit","body":124,"name":28,"type":79},"ie":125}
{"forallE":{"binderInfo":"implicit","body":125,"name":27,"type":76},"ie":126}
{"forallE":{"binderInfo":"implicit","body":126,"name":14,"type":75},"ie":127}
{"ie":128,"proj":{"idx":0,"struct":5,"typeName":24}}
{"ie":129,"lam":{"binderInfo":"instImplicit","body":128,"name":34,"type":96}}
{"ie":130,"lam":{"binderInfo":"implicit","body":129,"name":28,"type":79}}
{"ie":131,"lam":{"binderInfo":"default","body":130,"name":27,"type":76}}
{"ie":132,"lam":{"binderInfo":"default","body":131,"name":14,"type":75}}
{"def":{"all":[33],"hints":"abbrev","levelParams":[6,25,26],"name":33,"safety":"safe","type":127,"value":132}}
{"in":35,"str":{"pre":0,"str":"Add"}}
{"forallE":{"binderInfo":"default","body":75,"name":14,"type":75},"ie":133}
{"in":36,"str":{"pre":35,"str":"mk"}}
{"in":37,"str":{"pre":0,"str":"add"}}
{"forallE":{"binderInfo":"default","body":8,"name":19,"type":12},"ie":134}
{"forallE":{"binderInfo":"default","body":134,"name":19,"type":5},"ie":135}
{"const":{"name":35,"us":[2]},"ie":136}
{"app":{"arg":12,"fn":136},"ie":137}
{"forallE":{"binderInfo":"default","body":137,"name":37,"type":135},"ie":138}
{"forallE":{"binderInfo":"implicit","body":138,"name":14,"type":75},"ie":139}
{"in":38,"str":{"pre":35,"str":"rec"}}
{"app":{"arg":5,"fn":136},"ie":140}
{"forallE":{"binderInfo":"default","body":36,"name":8,"type":140},"ie":141}
{"forallE":{"binderInfo":"default","body":10,"name":19,"type":8},"ie":142}
{"forallE":{"binderInfo":"default","body":142,"name":19,"type":12},"ie":143}
{"const":{"name":36,"us":[2]},"ie":144}
{"app":{"arg":8,"fn":144},"ie":145}
{"app":{"arg":5,"fn":145},"ie":146}
{"app":{"arg":146,"fn":12},"ie":147}
{"forallE":{"binderInfo":"default","body":147,"name":37,"type":143},"ie":148}
{"app":{"arg":8,"fn":136},"ie":149}
{"forallE":{"binderInfo":"default","body":9,"name":8,"type":149},"ie":150}
{"forallE":{"binderInfo":"default","body":150,"name":32,"type":148},"ie":151}
{"forallE":{"binderInfo":"implicit","body":151,"name":7,"type":141},"ie":152}
{"forallE":{"binderInfo":"implicit","body":152,"name":14,"type":75},"ie":153}
{"forallE":{"binderInfo":"default","body":57,"name":19,"type":10},"ie":154}
{"forallE":{"binderInfo":"default","body":154,"name":19,"type":8},"ie":155}
{"ie":156,"lam":{"binderInfo":"default","body":25,"name":37,"type":155}}
{"ie":157,"lam":{"binderInfo":"default","body":156,"name":32,"type":148}}
{"ie":158,"lam":{"binderInfo":"default","body":157,"name":7,"type":141}}
{"ie":159,"lam":{"binderInfo":"default","body":158,"name":14,"type":75}}
{"inductive":{"ctors":[{"cidx":0,"induct":35,"isUnsafe":false,"levelParams":[6],"name":36,"numFields":1,"numParams":1,"type":139}],"recs":[{"all":[35],"isUnsafe":false,"k":false,"levelParams":[13,6],"name":38,"numIndices":0,"numMinors":1,"numMotives":1,"numParams":1,"rules":[{"ctor":36,"nfields":1,"rhs":159}],"type":153}],"types":[{"all":[35],"ctors":[36],"isRec":false,"isReflexive":false,"isUnsafe":false,"levelParams":[6],"name":35,"numIndices":0,"numNested":0,"numParams":1,"type":133}]}}
{"in":39,"str":{"pre":35,"str":"add"}}
{"forallE":{"binderInfo":"instImplicit","body":143,"name":34,"type":140},"ie":160}
{"forallE":{"binderInfo":"implicit","body":160,"name":14,"type":75},"ie":161}
{"ie":162,"proj":{"idx":0,"struct":5,"typeName":35}}
{"ie":163,"lam":{"binderInfo":"instImplicit","body":162,"name":34,"type":140}}
{"ie":164,"lam":{"binderInfo":"default","body":163,"name":14,"type":75}}
{"def":{"all":[39],"hints":"abbrev","levelParams":[6],"name":39,"safety":"safe","type":161,"value":164}}
{"in":40,"str":{"pre":0,"str":"instHAdd"}}
{"il":12,"succ":3}
{"ie":165,"sort":12}
{"in":41,"str":{"pre":0,"str":"inst"}}
{"in":42,"str":{"pre":41,"str":"_@"}}
{"in":43,"str":{"pre":42,"str":"Init"}}
{"in":44,"str":{"pre":43,"str":"Prelude"}}
{"in":45,"num":{"i":1910291827,"pre":44}}
{"in":46,"str":{"pre":45,"str":"_hygCtx"}}
{"in":47,"str":{"pre":46,"str":"_hyg"}}
{"in":48,"num":{"i":5,"pre":47}}
{"const":{"name":35,"us":[3]},"ie":166}
{"app":{"arg":5,"fn":166},"ie":167}
{"const":{"name":24,"us":[3,3,3]},"ie":168}
{"app":{"arg":12,"fn":168},"ie":169}
{"app":{"arg":12,"fn":169},"ie":170}
{"app":{"arg":12,"fn":170},"ie":171}
{"forallE":{"binderInfo":"instImplicit","body":171,"name":48,"type":167},"ie":172}
{"forallE":{"binderInfo":"implicit","body":172,"name":14,"type":165},"ie":173}
{"const":{"name":29,"us":[3,3,3]},"ie":174}
{"app":{"arg":12,"fn":174},"ie":175}
{"app":{"arg":12,"fn":175},"ie":176}
{"app":{"arg":12,"fn":176},"ie":177}
{"in":49,"str":{"pre":0,"str":"b"}}
{"const":{"name":39,"us":[3]},"ie":178}
{"app":{"arg":10,"fn":178},"ie":179}
{"app":{"arg":8,"fn":179},"ie":180}
{"app":{"arg":12,"fn":180},"ie":181}
{"app":{"arg":5,"fn":181},"ie":182}
{"ie":183,"lam":{"binderInfo":"default","body":182,"name":49,"type":8}}
{"ie":184,"lam":{"binderInfo":"default","body":183,"name":15,"type":12}}
{"app":{"arg":184,"fn":177},"ie":185}
{"ie":186,"lam":{"binderInfo":"instImplicit","body":185,"name":48,"type":167}}
{"ie":187,"lam":{"binderInfo":"implicit","body":186,"name":14,"type":165}}
{"def":{"all":[40],"hints":{"regular":1},"levelParams":[13],"name":40,"safety":"safe","type":173,"value":187}}
{"in":50,"str":{"pre":0,"str":"PUnit"}}
{"in":51,"str":{"pre":50,"str":"unit"}}
{"const":{"name":50,"us":[2]},"ie":188}
{"in":52,"str":{"pre":50,"str":"rec"}}
{"forallE":{"binderInfo":"default","body":36,"name":8,"type":188},"ie":189}
{"in":53,"str":{"pre":0,"str":"unit"}}
{"const":{"name":51,"us":[2]},"ie":190}
{"app":{"arg":190,"fn":5},"ie":191}
{"forallE":{"binderInfo":"default","body":9,"name":8,"type":188},"ie":192}
{"forallE":{"binderInfo":"default","body":192,"name":53,"type":191},"ie":193}
{"forallE":{"binderInfo":"implicit","body":193,"name":7,"type":189},"ie":194}
{"ie":195,"lam":{"binderInfo":"default","body":5,"name":53,"type":191}}
{"ie":196,"lam":{"binderInfo":"default","body":195,"name":7,"type":189}}
{"inductive":{"ctors":[{"cidx":0,"induct":50,"isUnsafe":false,"levelParams":[6],"name":51,"numFields":0,"numParams":0,"type":188}],"recs":[{"all":[50],"isUnsafe":false,"k":false,"levelParams":[13,6],"name":52,"numIndices":0,"numMinors":1,"numMotives":1,"numParams":0,"rules":[{"ctor":51,"nfields":0,"rhs":196}],"type":194}],"types":[{"all":[50],"ctors":[51],"isRec":false,"isReflexive":false,"isUnsafe":false,"levelParams":[6],"name":50,"numIndices":0,"numNested":0,"numParams":0,"type":3}]}}
{"in":54,"str":{"pre":0,"str":"PProd"}}
{"ie":197,"sort":4}
{"il":13,"max":[1,2]}
{"il":14,"max":[13,4]}
{"ie":198,"sort":14}
{"forallE":{"binderInfo":"default","body":198,"name":27,"type":197},"ie":199}
{"forallE":{"binderInfo":"default","body":199,"name":14,"type":3},"ie":200}
{"in":55,"str":{"pre":54,"str":"mk"}}
{"in":56,"str":{"pre":0,"str":"fst"}}
{"in":57,"str":{"pre":0,"str":"snd"}}
{"const":{"name":54,"us":[2,4]},"ie":201}
{"app":{"arg":10,"fn":201},"ie":202}
{"app":{"arg":8,"fn":202},"ie":203}
{"forallE":{"binderInfo":"default","body":203,"name":57,"type":12},"ie":204}
{"forallE":{"binderInfo":"default","body":204,"name":56,"type":12},"ie":205}
{"forallE":{"binderInfo":"implicit","body":205,"name":27,"type":197},"ie":206}
{"forallE":{"binderInfo":"implicit","body":206,"name":14,"type":3},"ie":207}
{"in":58,"str":{"pre":54,"str":"rec"}}
{"app":{"arg":12,"fn":201},"ie":208}
{"app":{"arg":5,"fn":208},"ie":209}
{"forallE":{"binderInfo":"default","body":36,"name":8,"type":209},"ie":210}
{"const":{"name":55,"us":[2,4]},"ie":211}
{"app":{"arg":57,"fn":211},"ie":212}
{"app":{"arg":10,"fn":212},"ie":213}
{"app":{"arg":12,"fn":213},"ie":214}
{"app":{"arg":5,"fn":214},"ie":215}
{"app":{"arg":215,"fn":8},"ie":216}
{"forallE":{"binderInfo":"default","body":216,"name":57,"type":8},"ie":217}
{"forallE":{"binderInfo":"default","body":217,"name":56,"type":8},"ie":218}
{"forallE":{"binderInfo":"default","body":9,"name":8,"type":203},"ie":219}
{"forallE":{"binderInfo":"default","body":219,"name":32,"type":218},"ie":220}
{"forallE":{"binderInfo":"implicit","body":220,"name":7,"type":210},"ie":221}
{"forallE":{"binderInfo":"implicit","body":221,"name":27,"type":197},"ie":222}
{"forallE":{"binderInfo":"implicit","body":222,"name":14,"type":3},"ie":223}
{"app":{"arg":12,"fn":8},"ie":224}
{"app":{"arg":5,"fn":224},"ie":225}
{"ie":226,"lam":{"binderInfo":"default","body":225,"name":57,"type":10}}
{"ie":227,"lam":{"binderInfo":"default","body":226,"name":56,"type":10}}
{"ie":228,"lam":{"binderInfo":"default","body":227,"name":32,"type":218}}
{"ie":229,"lam":{"binderInfo":"default","body":228,"name":7,"type":210}}
{"ie":230,"lam":{"binderInfo":"default","body":229,"name":27,"type":197}}
{"ie":231,"lam":{"binderInfo":"default","body":230,"name":14,"type":3}}
{"inductive":{"ctors":[{"cidx":0,"induct":54,"isUnsafe":false,"levelParams":[6,25],"name":55,"numFields":2,"numParams":2,"type":207}],"recs":[{"all":[54],"isUnsafe":false,"k":false,"levelParams":[13,6,25],"name":58,"numIndices":0,"numMinors":1,"numMotives":1,"numParams":2,"rules":[{"ctor":55,"nfields":2,"rhs":231}],"type":223}],"types":[{"all":[54],"ctors":[55],"isRec":false,"isReflexive":false,"isUnsafe":false,"levelParams":[6,25],"name":54,"numIndices":0,"numNested":0,"numParams":2,"type":200}]}}
{"in":59,"str":{"pre":1,"str":"below"}}
{"ie":232,"sort":13}
{"forallE":{"binderInfo":"default","body":232,"name":8,"type":1},"ie":233}
{"forallE":{"binderInfo":"implicit","body":233,"name":7,"type":4},"ie":234}
{"il":15,"succ":13}
{"const":{"name":5,"us":[15]},"ie":235}
{"ie":236,"lam":{"binderInfo":"default","body":232,"name":8,"type":1}}
{"app":{"arg":236,"fn":235},"ie":237}
{"const":{"name":50,"us":[13]},"ie":238}
{"app":{"arg":238,"fn":237},"ie":239}
{"const":{"name":54,"us":[2,13]},"ie":240}
{"app":{"arg":61,"fn":240},"ie":241}
{"app":{"arg":5,"fn":241},"ie":242}
{"ie":243,"lam":{"binderInfo":"default","body":242,"name":11,"type":232}}
{"ie":244,"lam":{"binderInfo":"default","body":243,"name":4,"type":1}}
{"app":{"arg":244,"fn":239},"ie":245}
{"app":{"arg":5,"fn":245},"ie":246}
{"ie":247,"lam":{"binderInfo":"default","body":246,"name":8,"type":1}}
{"ie":248,"lam":{"binderInfo":"implicit","body":247,"name":7,"type":4}}
{"def":{"all":[59],"hints":"abbrev","levelParams":[6],"name":59,"safety":"safe","type":234,"value":248}}
{"in":60,"str":{"pre":1,"str":"brecOn"}}
{"in":61,"str":{"pre":60,"str":"go"}}
{"in":62,"str":{"pre":0,"str":"F_1"}}
{"in":63,"str":{"pre":0,"str":"f"}}
{"const":{"name":59,"us":[2]},"ie":249}
{"app":{"arg":8,"fn":249},"ie":250}
{"app":{"arg":5,"fn":250},"ie":251}
{"forallE":{"binderInfo":"default","body":61,"name":63,"type":251},"ie":252}
{"forallE":{"binderInfo":"default","body":252,"name":8,"type":1},"ie":253}
{"app":{"arg":224,"fn":240},"ie":254}
{"app":{"arg":12,"fn":250},"ie":255}
{"app":{"arg":255,"fn":254},"ie":256}
{"forallE":{"binderInfo":"default","body":256,"name":62,"type":253},"ie":257}
{"forallE":{"binderInfo":"default","body":257,"name":8,"type":1},"ie":258}
{"forallE":{"binderInfo":"implicit","body":258,"name":7,"type":4},"ie":259}
{"const":{"name":5,"us":[13]},"ie":260}
{"app":{"arg":17,"fn":240},"ie":261}
{"app":{"arg":10,"fn":249},"ie":262}
{"app":{"arg":5,"fn":262},"ie":263}
{"app":{"arg":263,"fn":261},"ie":264}
{"ie":265,"lam":{"binderInfo":"default","body":264,"name":8,"type":1}}
{"app":{"arg":265,"fn":260},"ie":266}
{"const":{"name":55,"us":[2,13]},"ie":267}
{"app":{"arg":6,"fn":8},"ie":268}
{"app":{"arg":268,"fn":267},"ie":269}
{"app":{"arg":238,"fn":269},"ie":270}
{"const":{"name":51,"us":[13]},"ie":271}
{"app":{"arg":271,"fn":7},"ie":272}
{"app":{"arg":272,"fn":270},"ie":273}
{"app":{"arg":271,"fn":273},"ie":274}
{"app":{"arg":274,"fn":266},"ie":275}
{"app":{"arg":13,"fn":57},"ie":276}
{"app":{"arg":276,"fn":267},"ie":277}
{"app":{"arg":12,"fn":57},"ie":278}
{"app":{"arg":278,"fn":240},"ie":279}
{"app":{"arg":57,"fn":249},"ie":280}
{"app":{"arg":12,"fn":280},"ie":281}
{"app":{"arg":281,"fn":279},"ie":282}
{"app":{"arg":282,"fn":277},"ie":283}
{"app":{"arg":13,"fn":8},"ie":284}
{"app":{"arg":5,"fn":284},"ie":285}
{"app":{"arg":285,"fn":283},"ie":286}
{"app":{"arg":5,"fn":286},"ie":287}
{"ie":288,"lam":{"binderInfo":"default","body":287,"name":11,"type":264}}
{"ie":289,"lam":{"binderInfo":"default","body":288,"name":4,"type":1}}
{"app":{"arg":289,"fn":275},"ie":290}
{"app":{"arg":12,"fn":290},"ie":291}
{"ie":292,"lam":{"binderInfo":"default","body":291,"name":62,"type":253}}
{"ie":293,"lam":{"binderInfo":"default","body":292,"name":8,"type":1}}
{"ie":294,"lam":{"binderInfo":"implicit","body":293,"name":7,"type":4}}
{"def":{"all":[61],"hints":"abbrev","levelParams":[6],"name":61,"safety":"safe","type":259,"value":294}}
{"forallE":{"binderInfo":"default","body":224,"name":62,"type":253},"ie":295}
{"forallE":{"binderInfo":"default","body":295,"name":8,"type":1},"ie":296}
{"forallE":{"binderInfo":"implicit","body":296,"name":7,"type":4},"ie":297}
{"const":{"name":61,"us":[2]},"ie":298}
{"app":{"arg":8,"fn":298},"ie":299}
{"app":{"arg":12,"fn":299},"ie":300}
{"app":{"arg":5,"fn":300},"ie":301}
{"ie":302,"proj":{"idx":0,"struct":301,"typeName":54}}
{"ie":303,"lam":{"binderInfo":"default","body":302,"name":62,"type":253}}
{"ie":304,"lam":{"binderInfo":"default","body":303,"name":8,"type":1}}
{"ie":305,"lam":{"binderInfo":"implicit","body":304,"name":7,"type":4}}
{"def":{"all":[60],"hints":"abbrev","levelParams":[6],"name":60,"safety":"safe","type":297,"value":305}}
{"in":64,"str":{"pre":1,"str":"casesOn"}}
{"app":{"arg":6,"fn":12},"ie":306}
{"app":{"arg":5,"fn":11},"ie":307}
{"app":{"arg":307,"fn":10},"ie":308}
{"forallE":{"binderInfo":"default","body":308,"name":4,"type":1},"ie":309}
{"app":{"arg":8,"fn":10},"ie":310}
{"forallE":{"binderInfo":"default","body":310,"name":10,"type":309},"ie":311}
{"forallE":{"binderInfo":"default","body":311,"name":9,"type":306},"ie":312}
{"forallE":{"binderInfo":"default","body":312,"name":8,"type":1},"ie":313}
{"forallE":{"binderInfo":"implicit","body":313,"name":7,"type":4},"ie":314}
{"app":{"arg":12,"fn":27},"ie":315}
{"app":{"arg":5,"fn":57},"ie":316}
{"ie":317,"lam":{"binderInfo":"default","body":224,"name":11,"type":316}}
{"ie":318,"lam":{"binderInfo":"default","body":317,"name":4,"type":1}}
{"app":{"arg":318,"fn":315},"ie":319}
{"app":{"arg":8,"fn":319},"ie":320}
{"ie":321,"lam":{"binderInfo":"default","body":320,"name":10,"type":309}}
{"ie":322,"lam":{"binderInfo":"default","body":321,"name":9,"type":306}}
{"ie":323,"lam":{"binderInfo":"default","body":322,"name":8,"type":1}}
{"ie":324,"lam":{"binderInfo":"implicit","body":323,"name":7,"type":4}}
{"def":{"all":[64],"hints":"abbrev","levelParams":[6],"name":64,"safety":"safe","type":314,"value":324}}
{"in":65,"str":{"pre":1,"str":"add"}}
{"in":66,"str":{"pre":65,"str":"match_1"}}
{"in":67,"str":{"pre":0,"str":"x"}}
{"in":68,"str":{"pre":67,"str":"_@"}}
{"in":69,"str":{"pre":68,"str":"Init"}}
{"in":70,"str":{"pre":69,"str":"Prelude"}}
{"in":71,"num":{"i":2314059840,"pre":70}}
{"in":72,"str":{"pre":71,"str":"_hygCtx"}}
{"in":73,"num":{"i":13,"pre":72}}
{"in":74,"str":{"pre":73,"str":"Init"}}
{"in":75,"str":{"pre":74,"str":"Prelude"}}
{"in":76,"num":{"i":2314059840,"pre":75}}
{"in":77,"str":{"pre":76,"str":"_hygCtx"}}
{"in":78,"str":{"pre":77,"str":"_hyg"}}
{"in":79,"num":{"i":32,"pre":78}}
{"in":80,"num":{"i":14,"pre":72}}
{"in":81,"str":{"pre":80,"str":"Init"}}
{"in":82,"str":{"pre":81,"str":"Prelude"}}
{"in":83,"num":{"i":2314059840,"pre":82}}
{"in":84,"str":{"pre":83,"str":"_hygCtx"}}
{"in":85,"str":{"pre":84,"str":"_hyg"}}
{"in":86,"num":{"i":35,"pre":85}}
{"forallE":{"binderInfo":"default","body":36,"name":86,"type":1},"ie":325}
{"forallE":{"binderInfo":"default","body":325,"name":79,"type":1},"ie":326}
{"in":87,"str":{"pre":0,"str":"h_1"}}
{"app":{"arg":6,"fn":17},"ie":327}
{"forallE":{"binderInfo":"default","body":327,"name":15,"type":1},"ie":328}
{"in":88,"str":{"pre":0,"str":"h_2"}}
{"bvar":5,"ie":329}
{"app":{"arg":12,"fn":329},"ie":330}
{"app":{"arg":307,"fn":330},"ie":331}
{"forallE":{"binderInfo":"default","body":331,"name":49,"type":1},"ie":332}
{"forallE":{"binderInfo":"default","body":332,"name":15,"type":1},"ie":333}
{"app":{"arg":10,"fn":57},"ie":334}
{"app":{"arg":8,"fn":334},"ie":335}
{"forallE":{"binderInfo":"default","body":335,"name":88,"type":333},"ie":336}
{"forallE":{"binderInfo":"default","body":336,"name":87,"type":328},"ie":337}
{"forallE":{"binderInfo":"default","body":337,"name":86,"type":1},"ie":338}
{"forallE":{"binderInfo":"default","body":338,"name":79,"type":1},"ie":339}
{"forallE":{"binderInfo":"default","body":339,"name":7,"type":326},"ie":340}
{"const":{"name":64,"us":[3]},"ie":341}
{"app":{"arg":57,"fn":329},"ie":342}
{"app":{"arg":5,"fn":342},"ie":343}
{"ie":344,"lam":{"binderInfo":"default","body":343,"name":67,"type":1}}
{"app":{"arg":344,"fn":341},"ie":345}
{"app":{"arg":8,"fn":345},"ie":346}
{"app":{"arg":10,"fn":12},"ie":347}
{"app":{"arg":347,"fn":346},"ie":348}
{"in":89,"str":{"pre":4,"str":"_@"}}
{"in":90,"str":{"pre":89,"str":"Init"}}
{"in":91,"str":{"pre":90,"str":"Prelude"}}
{"in":92,"num":{"i":2314059840,"pre":91}}
{"in":93,"str":{"pre":92,"str":"_hygCtx"}}
{"in":94,"str":{"pre":93,"str":"_hyg"}}
{"in":95,"num":{"i":58,"pre":94}}
{"app":{"arg":57,"fn":12},"ie":349}
{"app":{"arg":5,"fn":349},"ie":350}
{"ie":351,"lam":{"binderInfo":"default","body":350,"name":95,"type":1}}
{"app":{"arg":351,"fn":348},"ie":352}
{"ie":353,"lam":{"binderInfo":"default","body":352,"name":88,"type":333}}
{"ie":354,"lam":{"binderInfo":"default","body":353,"name":87,"type":328}}
{"ie":355,"lam":{"binderInfo":"default","body":354,"name":86,"type":1}}
{"ie":356,"lam":{"binderInfo":"default","body":355,"name":79,"type":1}}
{"ie":357,"lam":{"binderInfo":"default","body":356,"name":7,"type":326}}
{"def":{"all":[66],"hints":"abbrev","levelParams":[13],"name":66,"safety":"safe","type":340,"value":357}}
{"in":96,"str":{"pre":65,"str":"_f"}}
{"in":97,"str":{"pre":72,"str":"_hyg"}}
{"in":98,"num":{"i":14,"pre":97}}
{"const":{"name":59,"us":[1]},"ie":358}
{"ie":359,"lam":{"binderInfo":"default","body":2,"name":98,"type":1}}
{"app":{"arg":359,"fn":358},"ie":360}
{"app":{"arg":5,"fn":360},"ie":361}
{"forallE":{"binderInfo":"default","body":2,"name":63,"type":361},"ie":362}
{"forallE":{"binderInfo":"default","body":362,"name":98,"type":1},"ie":363}
{"in":99,"num":{"i":13,"pre":97}}
{"const":{"name":66,"us":[1]},"ie":364}
{"in":100,"num":{"i":61,"pre":97}}
{"forallE":{"binderInfo":"default","body":1,"name":100,"type":361},"ie":365}
{"ie":366,"lam":{"binderInfo":"default","body":365,"name":86,"type":1}}
{"ie":367,"lam":{"binderInfo":"default","body":366,"name":79,"type":1}}
{"app":{"arg":367,"fn":364},"ie":368}
{"app":{"arg":5,"fn":368},"ie":369}
{"app":{"arg":8,"fn":369},"ie":370}
{"app":{"arg":6,"fn":360},"ie":371}
{"ie":372,"lam":{"binderInfo":"default","body":12,"name":100,"type":371}}
{"ie":373,"lam":{"binderInfo":"default","body":372,"name":15,"type":1}}
{"app":{"arg":373,"fn":370},"ie":374}
{"app":{"arg":307,"fn":360},"ie":375}
{"ie":376,"proj":{"idx":0,"struct":5,"typeName":54}}
{"app":{"arg":8,"fn":376},"ie":377}
{"app":{"arg":377,"fn":11},"ie":378}
{"ie":379,"lam":{"binderInfo":"default","body":378,"name":100,"type":375}}
{"ie":380,"lam":{"binderInfo":"default","body":379,"name":49,"type":1}}
{"ie":381,"lam":{"binderInfo":"default","body":380,"name":15,"type":1}}
{"app":{"arg":381,"fn":374},"ie":382}
{"app":{"arg":12,"fn":382},"ie":383}
{"ie":384,"lam":{"binderInfo":"default","body":383,"name":99,"type":1}}
{"ie":385,"lam":{"binderInfo":"default","body":384,"name":63,"type":361}}
{"ie":386,"lam":{"binderInfo":"default","body":385,"name":98,"type":1}}
{"def":{"all":[96],"hints":"abbrev","levelParams":[],"name":96,"safety":"safe","type":363,"value":386}}
{"forallE":{"binderInfo":"default","body":2,"name":19,"type":1},"ie":387}
{"const":{"name":60,"us":[1]},"ie":388}
{"app":{"arg":359,"fn":388},"ie":389}
{"app":{"arg":5,"fn":389},"ie":390}
{"const":{"name":96,"us":[]},"ie":391}
{"app":{"arg":391,"fn":390},"ie":392}
{"app":{"arg":12,"fn":392},"ie":393}
{"ie":394,"lam":{"binderInfo":"default","body":393,"name":98,"type":1}}
{"ie":395,"lam":{"binderInfo":"default","body":394,"name":99,"type":1}}
{"def":{"all":[65],"hints":{"regular":1},"levelParams":[],"name":65,"safety":"safe","type":387,"value":395}}
{"in":101,"str":{"pre":0,"str":"instAddNat"}}
{"const":{"name":35,"us":[0]},"ie":396}
{"app":{"arg":1,"fn":396},"ie":397}
{"const":{"name":36,"us":[0]},"ie":398}
{"app":{"arg":1,"fn":398},"ie":399}
{"const":{"name":65,"us":[]},"ie":400}
{"app":{"arg":400,"fn":399},"ie":401}
{"def":{"all":[101],"hints":{"regular":2},"levelParams":[],"name":101,"safety":"safe","type":397,"value":401}}
{"in":102,"str":{"pre":0,"str":"challenge_placeholder"}}
{"forallE":{"binderInfo":"implicit","body":5,"name":14,"type":3},"ie":402}
{"axiom":{"isUnsafe":false,"levelParams":[6],"name":102,"type":402}}
{"in":103,"str":{"pre":0,"str":"add_comm'"}}
{"const":{"name":12,"us":[1]},"ie":403}
{"app":{"arg":1,"fn":403},"ie":404}
{"const":{"name":33,"us":[0,0,0]},"ie":405}
{"app":{"arg":1,"fn":405},"ie":406}
{"app":{"arg":1,"fn":406},"ie":407}
{"app":{"arg":1,"fn":407},"ie":408}
{"const":{"name":40,"us":[0]},"ie":409}
{"app":{"arg":1,"fn":409},"ie":410}
{"const":{"name":101,"us":[]},"ie":411}
{"app":{"arg":411,"fn":410},"ie":412}
{"app":{"arg":412,"fn":408},"ie":413}
{"app":{"arg":12,"fn":413},"ie":414}
{"app":{"arg":5,"fn":414},"ie":415}
{"app":{"arg":415,"fn":404},"ie":416}
{"app":{"arg":5,"fn":413},"ie":417}
{"app":{"arg":12,"fn":417},"ie":418}
{"app":{"arg":418,"fn":416},"ie":419}
{"forallE":{"binderInfo":"default","body":419,"name":49,"type":1},"ie":420}
{"forallE":{"binderInfo":"default","body":420,"name":15,"type":1},"ie":421}
{"const":{"name":102,"us":[0]},"ie":422}
{"app":{"arg":419,"fn":422},"ie":423}
{"ie":424,"lam":{"binderInfo":"default","body":423,"name":49,"type":1}}
{"ie":425,"lam":{"binderInfo":"default","body":424,"name":15,"type":1}}
{"thm":{"all":[103],"levelParams":[],"name":103,"type":421,"value":425}}