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

[Sergei Meshveliani]

I mean pointwise equality over _≈_ rather than _≡_.


On Sun, 2019-03-10 at 22:42 +0300, Sergei Meshveliani wrote:
> 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
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>