[Agda] pointwise congr.of ++

[Nils Anders Danielsson]

On 2015-02-14 17:28, Sergei Meshveliani wrote:
> For the pointwise equality  _=l_  on  lists over any setoid  A,
> I program
>
>    ++cong-=l :  _++_ Preserves₂ _=l_ ⟶ _=l_ ⟶ _=l_
>
> Is this lemma in Standard library?

I don't think so.

-- 
/NAD