in
- Y1 t1 t2 ~~> elem1 elem1 elem2
+ X1 === Y1 t1 t2 ~~> elem1 elem1 elem2
=== (\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)
+ === t1 X1 X2
and
- Y2 t1 t2 ~~> elem2 elem1 elem2
+ X2 === Y2 t1 t2 ~~> elem2 elem1 elem2
=== (\elem1 elem2. t2 (elem1 elem1 elem2) (elem2 elem1 elems2)) elem1 elem2
~~> t2 (elem1 elem1 elem2) (elem2 elem1 elem2)
<~~> t2 (Y1 t1 t2) (Y2 t1 t2)
+ === t2 X1 X2