4 (\elem1 elem2. t1 (elem1 elem1 elem2) (elem2 elem1 elem2)) ; elem1
5 (\elem1 elem2. t1 (elem1 elem1 elem2) (elem2 elem1 elem2)) ; elem1
6 (\elem1 elem2. t2 (elem1 elem1 elem2) (elem2 elem1 elem2)) ; elem2
10 (\elem1 elem2. t2 (elem1 elem1 elem2) (elem2 elem1 elem2)) ; elem2
11 (\elem1 elem2. t1 (elem1 elem1 elem2) (elem2 elem1 elem2)) ; elem1
12 (\elem1 elem2. t2 (elem1 elem1 elem2) (elem2 elem1 elem2)) ; elem2
16 X1 === Y1 t1 t2 ~~> elem1 elem1 elem2
17 === (\elem1 elem2. t1 (elem1 elem1 elem2) (elem2 elem1 elems2)) elem1 elem2
18 ~~> t1 (elem1 elem1 elem2) (elem2 elem1 elem2)
19 <~~> t1 (Y1 t1 t2) (Y2 t1 t2)
24 X2 === Y2 t1 t2 ~~> elem2 elem1 elem2
25 === (\elem1 elem2. t2 (elem1 elem1 elem2) (elem2 elem1 elems2)) elem1 elem2
26 ~~> t2 (elem1 elem1 elem2) (elem2 elem1 elem2)
27 <~~> t2 (Y1 t1 t2) (Y2 t1 t2)