How to destruct H involving two variables

Using Rocq
,
1

Hi there!

I am trying to prove the following theorem:
image

image

How do I destruct H to remove the “forall a1 a2” part so that I can try to use H? I am unable to figure out the syntax. Can someone help me out?

Thanks!

2

You can use specialize (H arg1 arg2). Or destruct (H arg1 arg2) if you want to destruct it.

3

Hi!

Thank you so much for your reply! I tried it out but am getting the following error:

image