[Agda] exercice of Peter Dybjer

[Michel Levy]

In the paper AgdaLectureNotes2018
<http://www.cse.chalmers.se/~peterd/papers/AgdaLectureNotes2018.pdf> of
Peter Dybjer, there is this exercise page 19

Exercise: prove symmetry and transitivity using subst but without using
pattern matching!

I don't find the solution, can you help me to solve it ?

-- 
courriel : michel.levy.imag at free.fr
mobile : 06 59 13 42 53
web : michel.levy.imag.free.fr
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200322/1da16cf8/attachment.html>