we can use one more \exists in assoc-enough
[~helmut/bidiragda.git] / LiftGet.agda
2012-10-05 Helmut Grohnemove all postulates to one module
2012-09-27 Helmut Grohneremove getVec-getlen in favour of plain subst
2012-09-27 Helmut Grohnemove definition of get-type to BFF and use it everywhere
2012-09-18 Helmut GrohneMerge branch 'using-vec'
2012-09-14 Helmut Grohne\::-subst is a special case of subst-cong
2012-09-14 Helmut Grohnevec-len-via-list and length-toList are the same
2012-09-14 Helmut Grohnecomplete missing parts of LiftGet
2012-09-11 Helmut Grohneshow fromList-toList in the subst form
2012-09-11 Helmut GrohneLiftGet: replace vec-length-same with toList-subst
2012-09-10 Helmut GrohneLiftGet: vec-length is also known as subst (Vec A)
2012-09-04 Helmut Grohneformulate List <-> Vec isomorphism problems
2012-08-30 Helmut Grohneprove LiftGet.get-trafo-2-getlen
2012-08-30 Helmut Grohnephrase other half of bijection in LiftGet
2012-08-30 Helmut Grohneprove half of the bijection in LiftGet
2012-08-30 Helmut Grohnegive the type of different gets a name
2012-08-06 Helmut Grohneattempt isomorphism between get on List and on Vec