Move everything to old
[lambda.git] / hints / assignment_4_answer_4.mdwn
diff --git a/hints/assignment_4_answer_4.mdwn b/hints/assignment_4_answer_4.mdwn
deleted file mode 100644 (file)
index c2cd1fd..0000000
+++ /dev/null
@@ -1,29 +0,0 @@
-
-
-       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
-