{"push_id":1061120406,"size":2,"distinct_size":2,"ref":"refs/heads/wip","head":"cfab204598a528a597b4e73d4ec005d9f5a8836c","before":"1271039996d7f6ccf292db7dab7a52d2fb19231a","commits":[{"sha":"28aa8e9ca46ba7e4eeb914d3c18b75819f837dcb","author":{"email":"1f81e848faf55004077c594fb2256b536cb2c8e0@gmail.com","name":"Theo Belaire"},"message":"Moved all the definitions to the top and started using a module format","distinct":true,"url":"https://api.github.com/repos/tbelaire/FJ-Formalization/commits/28aa8e9ca46ba7e4eeb914d3c18b75819f837dcb"},{"sha":"cfab204598a528a597b4e73d4ec005d9f5a8836c","author":{"email":"1f81e848faf55004077c594fb2256b536cb2c8e0@gmail.com","name":"Theo Belaire"},"message":"Wip sub_strengthen\n\nSomething odd happens with inducting on H_sub","distinct":true,"url":"https://api.github.com/repos/tbelaire/FJ-Formalization/commits/cfab204598a528a597b4e73d4ec005d9f5a8836c"}]}