hints/assignment_4_answer_4.mdwn

   1
   2
   3         let Y1 = \t1 t2.
   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
   7                         in
   8
   9         let Y2 = \t1 t2.
  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
  13                         in
  14
  15
  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)
  20                          === t1 X1 X2
  21
  22                         and
  23
  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)
  28                          === t2 X1 X2
  29