[add] irrelevant & antisym to Pointwise for Data.Vec

[ruifengx]

List of Changes:

• Add irrelevant & antisym to Vec.Pointwise.Extensional
• Add irrelevant & antisym for Vec.Pointwise.Inductive
• Fix: relax sym & trans to allow different levels

I also checked the corresponding module in Data.List, and I found out that Data.List already have the corresponding definitions, but the naming is not consistent:

• Data.Vec uses refl, sym, trans (and here I add antisym)
• Data.List uses reflexive, symmetric, transitive, and antisymmetric

Perhaps the naming should be unified, but I do not know enough for this.

Regarding relaxing the level restrictions, symmtric and transitive in List.Pointwise is already level-polymorphic (the input relations R and S can have different levels) thanks to its use of generalisable variables.

[Taneb]

This all looks great! Can you add your changes to the changelog?

Regarding your point about naming, yes this should be unified, but that doesn't need to happen in this PR

[ruifengx]

Done. The CI is triggered again unfortunately. I will remember to do everything in one shot next time.