foldl-≗foldr∘reverse about agda-stdlib HOT 3 CLOSED

foldr-ys++y-eq : ∀ {α β} {A : Set α} {B : Set β} →
  (f : A → B → B) → (x : B) → (y : A) → (ys : List A) →
  foldr f x (ys ∷ʳ y) ≡ foldr f (f y x) ys

foldr-ys++y-eq _ _ _ []       =  PE.refl
foldr-ys++y-eq f x y (z ∷ ys) =  PE.cong (f z) $ foldr-ys++y-eq f x y ys

---

foldl≗foldr∘reverse : ∀ {α β} {A : Set α} {B : Set β} →
                              (f : A → B → B) → (x : B) → (ys : List A) →
                              foldl (flip f) x ys ≡ foldr f x (reverse ys)

foldl≗foldr∘reverse _ _  []       =  PE.refl
foldl≗foldr∘reverse f xs (y ∷ ys) =  
       PE.sym $
       ≡begin
         foldr f xs (reverse (y ∷ ys))      ≡[ PE.cong (foldr f xs)
                                                            rev-yys≡rev-ys++y ]
         foldr f xs ((reverse ys) ∷ʳ y)     ≡[ foldr-ys++y-eq f xs y
                                                                   (reverse ys) ]
         foldr f (f y xs) (reverse ys)       ≡[ PE.sym $ foldl≗foldr∘reverse
                                                                              f (f y xs) ys ]
         foldl ff (f y xs) ys
       ≡end
       where  rev-yys≡rev-ys++y =  unfold-reverse y ys
                   ff = flip f