=== (\elem1 elem2. t1 (elem1 elem1 elem2) (elem2 elem1 elems2)) elem1 elem2
~~> t1 (elem1 elem1 elem2) (elem2 elem1 elem2)
<~~> t1 (Y1 t1 t2) (Y2 t1 t2)
=== (\elem1 elem2. t1 (elem1 elem1 elem2) (elem2 elem1 elems2)) elem1 elem2
~~> t1 (elem1 elem1 elem2) (elem2 elem1 elem2)
<~~> t1 (Y1 t1 t2) (Y2 t1 t2)