+
+
+ let Y1 = \t1 t2.
+ (\elem1 elem2. t1 (elem1 elem1 elem2) (elem2 elem1 elem2)) ; elem1
+ (\elem1 elem2. t1 (elem1 elem1 elem2) (elem2 elem1 elem2)) ; elem1
+ (\elem1 elem2. t2 (elem1 elem1 elem2) (elem2 elem1 elem2)) ; elem2
+ in
+
+ let Y2 = \t1 t2.
+ (\elem1 elem2. t2 (elem1 elem1 elem2) (elem2 elem1 elem2)) ; elem2
+ (\elem1 elem2. t1 (elem1 elem1 elem2) (elem2 elem1 elem2)) ; elem1
+ (\elem1 elem2. t2 (elem1 elem1 elem2) (elem2 elem1 elem2)) ; elem2
+ in
+
+
+ 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)
+
+ and
+
+ 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)
+