Compare lists by relation

Stream: lean4

[Marcus Rossel]

Say we have two lists l1 : List X, l2 : List Y and a relation r : X -> Y -> Prop.
Is there a nice way of expressing that for each index i: l1[i] and l2[i] satisfy relation r?
If l1 and l2 do not have the same length, the overall proposition should be false.

[Mario Carneiro]

docs#list.forall₂

[Marcus Rossel]

Beautiful! Thanks :)