employ insertionresult in lemma-lookupM-checkInsert
[~helmut/bidiragda.git] / Precond.agda
2013-01-10 Helmut Grohneclean imports of Precond
2013-01-10 Helmut Grohneuse different formulation of all-different
2012-12-14 Helmut Grohneun-inline different-drop
2012-11-19 Helmut Grohnewe can also drop an implicit parameter from assoc-enough
2012-11-19 Helmut Grohnewe can use one more \exists in assoc-enough
2012-11-19 Helmut Grohnestrip prose from assoc-enough
2012-10-22 Helmut GrohneMerge branch 'modparam'
2012-10-22 Helmut Grohnefinally parameterize CheckInsert
2012-10-22 Helmut Grohnenow parameterize BFF
2012-10-22 Helmut Grohnealso parameterize Precond
2012-09-27 Helmut Grohnemove definition of get-type to BFF and use it everywhere
2012-09-26 Helmut Grohnerename suc-\== to suc-injective
2012-09-18 Helmut GrohneMerge branch 'using-vec'
2012-09-08 Helmut Grohnegive a sufficient precondition for theorem-2