Start the proof that ua implies funext
authorAnders Mörtberg <mortberg@chalmers.se>
Thu, 9 Apr 2015 20:58:11 +0000 (22:58 +0200)
committerAnders Mörtberg <mortberg@chalmers.se>
Thu, 9 Apr 2015 20:58:11 +0000 (22:58 +0200)
commit4261c6af1575aa286a71b2ae30d696da4bd3a7a3
treee00b7d3415ea16efa39c4c051ea8198475d049e4
parentd45829ab83fff9670434f4a718afc477f7f6ac1b
Start the proof that ua implies funext
examples/uafunext.ctt [new file with mode: 0644]