Investigate a leftward arrow

[jeremie-koenig]

We could investigate a "leftward" variant of the arrow relator such as:

(R <== S) f g  :=  forall x y, S (f x) (g y) -> R x y

This would be useful to formulate injectivity-like properties. In particular for the relators of inductive types, the injectivity of constructors could be expressed in this way, and declaring the corresponding relational properties could help us mechanize the automatic decomposition of hypotheses such as for example:

 list_rel R (x1 :: x2 :: l) (y1 :: y2 :: l')
---------------------------------------------
    R x1 y1 /\ R x2 y2 /\ list_rel R l l'

Unfortunately, the relator as defined above does not behave in a good way with curried function. So for example:

Proper (R <== list_rel R <== list_rel R) cons

does not encode the property that we want (in fact the corresponding property is false).

It is not immediately obvious how to solve this problem (other than using rel_curry each time we want to state such a property as R * list_rel R <== list_rel R).