convert LiftGet module to using heterogeneous equality
authorHelmut Grohne <grohne@cs.uni-bonn.de>
Wed, 26 Feb 2014 08:16:19 +0000 (09:16 +0100)
committerHelmut Grohne <grohne@cs.uni-bonn.de>
Wed, 26 Feb 2014 08:16:19 +0000 (09:16 +0100)
commit28e7397a76be229ba723e49db51d2bf0b87c5493
tree809131bc5b5afbfc6d6e6a34b957e22a1d0a446c
parent8d0659f5dcfec4fc75096aa188c99af35c23bad5
convert LiftGet module to using heterogeneous equality

The reduction in proof length is impressive.
LiftGet.agda