Adds the AVL tree's toList/Any properties

[mikedelorimier]

This adds

toList⁺ : Any P t → List.Any P (toList t)
toList⁻ : List.Any P (toList t) → Any P t

These use a relation that states that the AVL's toList and toDiffList are equivalent:

toList∼toDiffList : ∀ t → toList t ∼ toDiffList t

I also added lemmas to Data.DifferenceList.Properties:

toList-refl : xs ∼ ys → toList ys ∼ ys
toList-++ : xs₁ ∼ ys₁ → (ys₂ : DiffList A) → xs₁ List.++ toList ys₂ ≡ toList (ys₁ ++ ys₂)

These let the DiffList user reason about the correspond between List and DiffList. Lower-level reasoning that uses the definition of DiffList as a function, or the definitions of toList and fromList as appends is hidden in toList-refl and toList-++. It seemed helpful to hide this reasoning at the risk of adding lemmas that seem ad-hoc.

[jamesmckinna]

Thanks @mikedelorimier this looks good, but I think could be tightened up in a number of places.

[jamesmckinna]

Lots more nitpicking... sorry for that, but I think each suggestion is a (potential!?) improvement. So I won't insist on them, but...

[mikedelorimier]

Lots more nitpicking... sorry for that, but I think each suggestion is a (potential!?) improvement. So I won't insist on them, but...

All your comments made sense to me, and I updated the code accordingly.

[jamesmckinna]

All looks good, let's see if we can get a second review! @gallais for example?