formulate List <-> Vec isomorphism problems
authorHelmut Grohne <helmut@subdivi.de>
Tue, 4 Sep 2012 06:42:38 +0000 (08:42 +0200)
committerHelmut Grohne <helmut@subdivi.de>
Tue, 4 Sep 2012 06:42:38 +0000 (08:42 +0200)
commitbd2a63675bb859e42d9e1464ff9a7883884c1fd5
tree08d70e85b7016ae81376f945c3f905f809b05ff2
parent22d4d452aaee82744c57f063b3416fd67df736c2
formulate List <-> Vec isomorphism problems

There are now like four open holes in LiftGet.agda that all boil down to
the same problem. For proving equalities on Vec we first need to show
that those Vecs actually have the same type. Proofs on two different
levels are needed and somehow need to be merged.
LiftGet.agda