started proving theorem-1
authorHelmut Grohne <helmut@subdivi.de>
Thu, 9 Feb 2012 11:35:10 +0000 (12:35 +0100)
committerHelmut Grohne <helmut@subdivi.de>
Thu, 9 Feb 2012 11:35:10 +0000 (12:35 +0100)
commit7309d04bb2eb5bfcbf9eb1e7f1f92fc1bdd470f2
tree905bec1b00b5c8339cc8adc98caf579f7fc67c26
parenteb6be3f9358e441fcee9256da5aae8915453f0a5
started proving theorem-1

As in the bff paper expand s using lemma-map-denumerate-enumerate
and apply free-theorem-list-list to commute get and map.
Bidir.agda