[Agda] pontwise ++-cong, reverse-cong

[Sergei Meshveliani]

Dear standard library developers,

has the library proofs for  ++-cong, reverse-cong 
for the pointwise equality on lists
(for _++_ and `reverse' respectvely) ?

If it has not, then may be it needs to have such
(may be together with some other `-cong' items for the pointwise
equality) ?

Thanks,

------
Sergei