assign 4: no hint for enum fringe
[lambda.git] / 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