{"entities":{"Q2819193":{"pageid":2829931,"ns":120,"title":"Item:Q2819193","lastrevid":83585345,"modified":"2026-05-07T09:08:48Z","type":"item","id":"Q2819193","labels":{"en":{"language":"en","value":"Some Wellfounded Trees in UniMath"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6630637"}},"aliases":{},"claims":{"P31":[{"mainsnak":{"snaktype":"value","property":"P31","hash":"fd5912e4dab4b881a8eb0eb27e7893fef55176ad","datavalue":{"value":{"entity-type":"item","numeric-id":56887,"id":"Q56887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2819193$5BBFC3C2-16DB-467C-847F-77858D661AD2","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"f4c77dcde6d717261f79d61171704dbbb44385d9","datavalue":{"value":{"text":"Some Wellfounded Trees in UniMath","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2819193$C80A8AF2-B766-43CC-8249-76C787E223A4","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"8a3d0cb3e0ee3ab03eded662b3b5d68448838d05","datavalue":{"value":"1434.03023","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2819193$1F0676AF-4FB1-4364-B97E-BF08DB37A4A2","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"04f48b8ca5c8f233d3253bf779c9fc98088de700","datavalue":{"value":"10.1007/978-3-319-42432-3_2","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2819193$83119862-4829-41D6-BE4B-5B136D39D552","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"6ebdd912b169a139b5481c76e8978f5a1ad20396","datavalue":{"value":{"entity-type":"item","numeric-id":2319988,"id":"Q2319988"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2819193$742179B0-998D-4744-A050-A2C6F5B6C216","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"37b6655ff0c1854542b6f28c9af39f0877a44635","datavalue":{"value":{"entity-type":"item","numeric-id":2319989,"id":"Q2319989"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2819193$1069638C-8692-43C1-BC3C-F9C4228FEA72","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"5ce1d49245d97a30ecabe94a0469a6616f4841aa","datavalue":{"value":{"entity-type":"item","numeric-id":2819192,"id":"Q2819192"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2819193$8B0B2DB5-8B09-460E-95A7-B08975FCBD64","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"300772c5a0b58bf4f4bfdafa9010450cf2acf8fe","datavalue":{"value":{"time":"+2016-09-28T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2819193$888692B5-21B6-4987-B417-0D525CA9C1A6","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2819193$67297221-BE9A-4464-B0CC-E6C07CCFBC23","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d9230c8da6e5632ad621620269b7ca185454f9df","datavalue":{"value":"03B38","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2819193$B1C1DB19-4DE9-48D4-85AD-AEFBE1C9502F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"58b3a5d0bc4bfd215423308dfe52b6887acdeedd","datavalue":{"value":"68V20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2819193$FB1513EF-B347-486E-A3B6-65986047B17A","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"e5cb43c240132a6004a89427aaeab990f6f640a7","datavalue":{"value":"6630637","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2819193$CE423CEB-9B44-43DA-B4F3-EC1E05D7D5C6","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c6a78675f0dcb3af511ac1d4dfa61901e828bcb8","datavalue":{"value":"proof assistant","type":"string"},"datatype":"string"},"type":"statement","id":"Q2819193$89DF6A7D-BBE9-4025-B561-0E9BEFE9FA86","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e55b3b4777557b818df7e0a13a733ea5bfaf8dee","datavalue":{"value":"univalent type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q2819193$C26A54AA-4411-4666-8189-129EC4E63574","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9261e7176c355d25de550288f511ceb3b62960f2","datavalue":{"value":"inductive datatypes","type":"string"},"datatype":"string"},"type":"statement","id":"Q2819193$3C4B3842-110A-4D8C-A1CE-534948DF2045","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1c131662411c2c68489cd24fb9f1ab517f584f48","datavalue":{"value":"UniMath","type":"string"},"datatype":"string"},"type":"statement","id":"Q2819193$293EBA99-F65A-486C-8BD3-C186D05EA8C6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ae973dea0bce1781f54a2b7f8606c1e8a434cfdd","datavalue":{"value":"initial algebras","type":"string"},"datatype":"string"},"type":"statement","id":"Q2819193$F6D41193-D5DD-48A6-AF0D-EFA4AFDA3C52","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a94daa7865c51c0d2412cced8422ea9361d06e30","datavalue":{"value":{"entity-type":"item","numeric-id":21343,"id":"Q21343"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2819193$74F3D636-A33C-43C7-A03F-89560E59B17D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ab6ee58efeeaa685ac2b8ecf828badcfb673e8c7","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2819193$99EC47AB-F9A8-4D8D-9AF9-E4AB54C294DE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b69ae52d53a05f3f4bf4d99cc0f83e03b73ae561","datavalue":{"value":{"entity-type":"item","numeric-id":27033,"id":"Q27033"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2819193$63A75D01-135F-4FDB-94CA-EA9D51BE36AD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b29eb58b948f9f996cbb5eae736ddbdaf0434b06","datavalue":{"value":{"entity-type":"item","numeric-id":34514,"id":"Q34514"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2819193$4885CD3B-6425-4CDF-9F55-7557056B4DD6","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"57f7fea50d2ce1b39b695c4a1313582eed405e38","datavalue":{"value":{"entity-type":"item","numeric-id":5976449,"id":"Q5976449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2819193$7D20F687-8A42-4E86-9E5C-4523B725DAA0","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"b7368fb27112381f18f110555cbe827a8430a826","datavalue":{"value":"https://doi.org/10.1007/978-3-319-42432-3_2","type":"string"},"datatype":"url"},"type":"statement","id":"Q2819193$91FA292B-9664-4C78-8305-9401E93712D2","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"38cdc70e07a211387c62f9c974de1c146ee76e7f","datavalue":{"value":"W2475593741","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2819193$0D707DD4-964C-42BC-ADD0-9151D4D2DDE9","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"9bc708db8417b264ae5134e14d7f4436923047c5","datavalue":{"value":{"entity-type":"item","numeric-id":4044767,"id":"Q4044767"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2819193$DCB89D36-804A-4F4E-AC70-5304AB772DA8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b0473ed6d7fc7ca641b0df021e4eef65b253f7a9","datavalue":{"value":{"entity-type":"item","numeric-id":5277827,"id":"Q5277827"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2819193$65AD5BF2-0D56-4672-AAA7-1BD853DD8FFE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7bcf33a5f992d181e7e78bbd8db6166cca7b5d2d","datavalue":{"value":{"entity-type":"item","numeric-id":5740648,"id":"Q5740648"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2819193$4DA86AC4-5BBD-45AC-84A5-094F6252ED47","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"89a306c39e90a61bbf0324324b38f286a3808406","datavalue":{"value":{"entity-type":"item","numeric-id":2986785,"id":"Q2986785"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2819193$A1810DF6-589C-4807-A9A3-02B7BA29BD0D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"468e91b711762444f3218471e1feccac4a79e420","datavalue":{"value":{"entity-type":"item","numeric-id":2968413,"id":"Q2968413"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2819193$7955CAAE-7FDD-4B59-9434-59E519CD1671","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5a797407b4949355fcd06204fe2bcb7b1218a925","datavalue":{"value":{"entity-type":"item","numeric-id":4256148,"id":"Q4256148"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2819193$2A6EDD2F-D6EB-4F77-9280-271B93B69056","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a4fd098ea4c8653eaec826e6d53d5157343c914f","datavalue":{"value":{"entity-type":"item","numeric-id":4580226,"id":"Q4580226"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2819193$B73F1D6F-05D1-421B-9B5B-46B0BC292690","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d43f11a5e6fc21caa581e9ac1e35682b1839d73e","datavalue":{"value":{"entity-type":"item","numeric-id":3075246,"id":"Q3075246"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2819193$A8C2F4D7-1AE1-400B-9926-56603FC99F65","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bdf4ccdcc70e71d35fd15b371cfa64eecb3f47f9","datavalue":{"value":{"entity-type":"item","numeric-id":4215784,"id":"Q4215784"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2819193$B3A8310E-0BE5-4B21-86E1-9E47194F24AC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3b98e59524c09aa47e1d06221dbbb46b4da0c230","datavalue":{"value":{"entity-type":"item","numeric-id":703526,"id":"Q703526"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2819193$FAB50A66-B8F6-4748-AD97-D761B3B58191","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9483d0139d2bb4d0d243ab47c468e3ad05746c57","datavalue":{"value":{"entity-type":"item","numeric-id":5740657,"id":"Q5740657"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2819193$7BA848CE-1A4F-4479-9F82-EE53C57C1592","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ebdb0b8e9e5d5193d9ae8203765dfde6514af006","datavalue":{"value":{"entity-type":"item","numeric-id":3001428,"id":"Q3001428"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c011956489ae1b816c54c99019b1bc926cfe7806","datavalue":{"value":{"amount":"+0.8852764","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2819193$12993B7C-701F-477F-B91F-D95ACFA68D71","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d8110f59ecbaf66a0b85041dbacf5b38a00c7046","datavalue":{"value":{"entity-type":"item","numeric-id":2958515,"id":"Q2958515"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"18de47730f0e0c2b3aa3d1238baeb2fa54990896","datavalue":{"value":{"amount":"+0.8732312","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2819193$C92CDFC5-6FF3-41D7-92F6-80F45C8141C3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9171693f573bbc066ee71cbfdb87707934542684","datavalue":{"value":{"entity-type":"item","numeric-id":1825187,"id":"Q1825187"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c486e874ed8303cf2b81bff44731ea0fd20b622d","datavalue":{"value":{"amount":"+0.87169945","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2819193$8D8B3223-5262-4D73-AAB9-5CE3C33939E9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7498b79849581123d6c3306bce74fe5fcfa7fc86","datavalue":{"value":{"entity-type":"item","numeric-id":1352126,"id":"Q1352126"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"db68e8bc315e6e84ece9f2a1fb075d88fead92c3","datavalue":{"value":{"amount":"+0.8699272","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2819193$3BA7795C-19E5-4EEF-AF39-A9F8BAE694FE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f351771d4a4383749827af0e39bb9acab55daf30","datavalue":{"value":{"entity-type":"item","numeric-id":3128469,"id":"Q3128469"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fb2cbf7a2c5f0b4af397e618ad2e20898805ad6b","datavalue":{"value":{"amount":"+0.8655091","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2819193$9C291585-288B-4004-AD05-4768593A2826","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0f4611beadcec1b05fef542b3dbb0e79ec75c1b1","datavalue":{"value":{"entity-type":"item","numeric-id":1340213,"id":"Q1340213"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"826d2ad849a438b50b5786bb39707eaba11c4fdb","datavalue":{"value":{"amount":"+0.8598231","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2819193$9921559D-794F-4672-A975-B3A96722C1A8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0a9263989c5686e92a41bfc6ab08ad140cfbaedb","datavalue":{"value":{"entity-type":"item","numeric-id":4430893,"id":"Q4430893"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"40af0e05a5aa0fccb38a6658fb30f13d70704c44","datavalue":{"value":{"amount":"+0.85915303","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2819193$DF80B6A9-F1D0-4BAA-BC46-2D89ABB5EF4B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c1d2ee127d3c56a27bc1ae00b613f275b2079a6e","datavalue":{"value":{"entity-type":"item","numeric-id":5051466,"id":"Q5051466"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2626addd1051a704aa52d0489d2aed604f7ae8dd","datavalue":{"value":{"amount":"+0.8574548","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2819193$2FC25EDC-4761-42D1-8359-7F0733DE6277","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a32a6a8b2fa1d923041153544028775a1677249a","datavalue":{"value":{"entity-type":"item","numeric-id":5712306,"id":"Q5712306"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"bb62f93536caa320f7ca1e0ae872c0ca1ad5ceb0","datavalue":{"value":{"amount":"+0.8527549","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2819193$0715AB44-012F-4D6E-B939-35AD8B57D8E9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"56c536187255a15b1b91b693a53c70adac2fc377","datavalue":{"value":{"entity-type":"item","numeric-id":2222962,"id":"Q2222962"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ed9f112ebeef3366bddf19ae8170319246f4a09a","datavalue":{"value":{"amount":"+0.85206753","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2819193$C798230B-A52B-4D80-BE61-EC36152FCECA","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Some Wellfounded Trees in UniMath","badges":[]}}}}}