inline bot-elim into lemma-just-nothing
authorHelmut Grohne <helmut@subdivi.de>
Tue, 17 Apr 2012 10:10:35 +0000 (12:10 +0200)
committerHelmut Grohne <helmut@subdivi.de>
Tue, 17 Apr 2012 10:10:35 +0000 (12:10 +0200)
commitdabd8455638d0cea486dd94dcdd13729077018d7
tree79ece5f9819424200f555fd12e2df13a865d3d00
parentf429f2e2027fc75e3d40f4be43322fa02bb3ab8c
inline bot-elim into lemma-just-nothing

Seems like the more common use case.
Bidir.agda