parameterize Bidir via Carrier and deq
[~helmut/bidiragda.git] / CheckInsert.agda
2012-09-26 Helmut Grohneuse _\==n_ and _\notin_ instead of \neg
2012-09-26 Helmut Grohneimport [_] instead of Reveal_is_
2012-09-18 Helmut GrohneMerge branch 'using-vec'
2012-09-18 Helmut Grohneone more application of lemma-just\==nnothing
2012-06-05 Helmut Grohnemove checkInsert and related properties to CheckInsert...