[Agda] Need help completing a proof

[Miëtek Bak]

In this case, the simplest solution seems to be using with-abstraction to pattern match on the result of `equation`, in order to let Agda take the desired equality `G ≡ H` into account.
https://agda.readthedocs.io/en/latest/language/with-abstraction.html

```diff
--- Example-before.lagda.md
+++ Example-after.lagda.md
@@ -147 +147,2 @@
-example g h p q s t M e = {!!}
+example g h p q s t M e with equation g h p q s t e
+... | refl = ⟨ (M ↑ p) ↓ q , collapse g h ⟩
```

-- 
MB


On Fri, Dec 24, 2021, at 18:03, Philip Wadler wrote:
> I'm having trouble completing a proof, and would be grateful for help. 
> The problem arises because I need to show two values are equal, but the 
> equality of the values follows from a complex equation. In fact, it is 
> not hard to show that the equality follows from the equation, but when 
> I attempt to use the desired equality for rewriting Agda complains and 
> I can't work out what it is complaining about (or how to fix it).
>
> A complete example is attached. The original is more complex, I've 
> tried to boil it down to its simplest form. My apologies that the 
> simplest form is not so simple!
>
> Thank you for your help. Go well, -- P
>
>
>
> .   \ Philip Wadler, Professor of Theoretical Computer Science,
> .   /\ School of Informatics, University of Edinburgh
> .  /  \ and Senior Research Fellow, IOHK
> . http://homepages.inf.ed.ac.uk/wadler/
>
> The University of Edinburgh is a charitable body, registered in
> Scotland, with registration number SC005336.
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
> Attachments:
> * Example.lagda.md