complete missing parts of LiftGet
authorHelmut Grohne <helmut@subdivi.de>
Fri, 14 Sep 2012 12:00:57 +0000 (14:00 +0200)
committerHelmut Grohne <helmut@subdivi.de>
Fri, 14 Sep 2012 12:00:57 +0000 (14:00 +0200)
commit27cf65ec6fe7c83d53fc8f9c4383041a5af882a2
treeff3a7c51d0a86328a31df800c7901addf37836b5
parent585ebc3a11db7b6544817b6f527efcba48982d6c
complete missing parts of LiftGet

Thanks to Joachim Breitner and Wouter Swierstra for their encouragement
and hints. Note that the result duplicates work at this point, but the
proofs are complete.
LiftGet.agda