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

[Guillaume Allais]

Hi Sergei,

Is this what you are looking for?
https://agda.github.io/agda-stdlib/Data.List.Relation.Binary.Pointwise.html#7371

++⁺ : ∀ {ws xs ys zs} → Pointwise _∼_ ws xs → Pointwise _∼_ ys zs →
        Pointwise _∼_ (ws ++ ys) (xs ++ zs)

Cheers,
--
gallais

On 10/03/2019 20:42, 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
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: OpenPGP digital signature
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190311/92da6877/attachment.sig>