+++ /dev/null
-
-
- 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
-
-
- 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
-
- 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
-